proposition: Lemma morphim_comp (A : {set gT}) : gof @* A = g @* (f @* A).
proof: Proof. apply/setP=> z; apply/morphimP/morphimP=> [[x]|[y Hy fAy ->{z}]]. rewrite !inE => /andP[Gx Hfx]; exists (f x) => //. by apply/morphimP; exists x. by case/morphimP: fAy Hy => x Gx Ax ->{y} Hfx; exists x; rewrite ?inE ?Gx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)