let G, H be Ring; for f being Function of G,H st f is linear holds
RingMorphismStr(# G,H,f #) is Morphism of G,H
let f be Function of G,H; ( f is linear implies RingMorphismStr(# G,H,f #) is Morphism of G,H )
assume A1:
f is linear
; RingMorphismStr(# G,H,f #) is Morphism of G,H
set F = RingMorphismStr(# G,H,f #);
A2:
fun RingMorphismStr(# G,H,f #) = f
;
( dom RingMorphismStr(# G,H,f #) = G & cod RingMorphismStr(# G,H,f #) = H )
;
hence
RingMorphismStr(# G,H,f #) is Morphism of G,H
by A1, A2, Lm4; verum