proposition: Lemma morphimSGK A G : A \subset D -> 'ker f \subset G -> (f @* A \subset f @* G) = (A \subset G).
proof: Proof. by move=> sGD skfK; rewrite morphimSK // mulSGid. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)