let G, H be Ring; :: thesis: 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; :: thesis: ( f is linear implies RingMorphismStr(# G,H,f #) is Morphism of G,H )
assume A1: f is linear ; :: thesis: 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; :: thesis: verum