let G, H be Ring; :: thesis: for f being strict RingMorphismStr st dom f = G & cod f = H & fun f is linear holds
f is Morphism of G,H
let f be strict RingMorphismStr ; :: thesis: ( dom f = G & cod f = H & fun f is linear implies f is Morphism of G,H )
assume A1: ( dom f = G & cod f = H & fun f is linear ) ; :: thesis: f is Morphism of G,H
then reconsider f' = f as RingMorphism by Def6;

now

( dom f' = G & cod f' = H ) by A1;
hence G <= H by Def8; :: thesis: verum

end;

then f' is Morphism of G,H by A1, Def9;
hence f is Morphism of G,H ; :: thesis: verum