proposition: Lemma eq_in_morphim B A (g : {morphism B >-> rT}) : D :&: A = B :&: A -> {in A, f =1 g} -> f @* A = g @* A.
proof: Proof. move=> eqDBA eqAfg; rewrite /morphim /= eqDBA. by apply: eq_in_imset => x /setIP[_]/eqAfg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)