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 Def6;
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 GRCAT_1:def 13; :: according to GRCAT_1:def 13,RINGCAT1:def 2,RINGCAT1:def 6 :: 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 GROUP_6:def 7, A1; :: according to GROUP_6:def 7 :: 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