proposition: Lemma morphim_homg aT rT (A D : {set aT}) (f : {morphism D >-> rT}) : A \subset D -> homg (f @* A) A.
proof: Proof. move=> sAD; apply/homgP; exists (restrm_morphism sAD f). by rewrite morphim_restrm setIid. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)