proposition: Lemma morphimDG A G : 'ker f \subset G -> f @* (A :\: G) = f @* A :\: f @* G.
proof: Proof. move=> sKG; apply/eqP; rewrite eqEsubset morphimD andbT !setDE subsetI. rewrite morphimS ?subsetIl // -[~: f @* G]setU0 -subDset setDE setCK. by rewrite -morphimIG //= setIAC -setIA setICr setI0 morphim0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)