proposition: Lemma domP (f : {morphism D >-> rT}) : 'dom f = A -> {g : {morphism A >-> rT} | [/\ g = f :> (aT -> rT), 'ker g = 'ker f, forall R, g @*^-1 R = f @*^-1 R & forall B, g @* B = f @* B]}.
proof: Proof. by move <-; exists f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)