let F be RingMorphism; :: thesis: RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is RingMorphism-like
set S = RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #);
A1: fun F is linear by Def5;
hence for x, y being Scalar of the Dom of RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) holds (fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . (x + y) = ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . x) + ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . y) by VECTSP_1:def 20; :: according to VECTSP_1:def 19,RINGCAT1:def 1,RINGCAT1:def 5 :: thesis: ( fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is multiplicative & fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is unity-preserving )
thus for x, y being Scalar of the Dom of RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) holds (fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . (x * y) = ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . x) * ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . y) by A1, GROUP_6:def 6; :: according to GROUP_6:def 6 :: thesis: fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is unity-preserving
thus fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is unity-preserving by A1; :: thesis: verum