proposition: Lemma morphimF gT rT (G D : {group gT}) (f : {morphism D >-> rT}) : G \subset D -> f @* (F gT G) \subset F rT (f @* G).
proof: Proof. move=> sGD; rewrite -(setIidPr (gFsub F G)). by rewrite -{3}(setIid G) -!(morphim_restrm sGD) gFcont. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)