proposition: Lemma restr_isom_to (A : {set aT}) (C R : {group rT}) (sAG : A \subset G) : f @* A = C -> isom G R f -> isom A C (restrm sAG f).
proof: Proof. by move=> defC /isomP[inj_f _]; apply: sub_isom. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)