proposition: Lemma restrmP (f : {morphism D >-> rT}) : A \subset 'dom f -> {g : {morphism A >-> rT} | [/\ g = f :> (aT -> rT), 'ker g = 'ker_A f, forall R, g @*^-1 R = A :&: f @*^-1 R & forall B, B \subset A -> g @* B = f @* B]}.
proof: Proof. move=> sAD; exists (restrm_morphism sAD f). split=> // [|R|B sBA]; first 1 [exact: ker_restrm | exact: morphpre_restrm]. by rewrite morphim_restrm (setIidPr sBA). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)