let F be RingMorphism; 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; VECTSP_1:def 19,RINGCAT1:def 1,RINGCAT1:def 5 ( 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; GROUP_6:def 6 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; verum