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 that
A1: dom f = G and
A2: cod f = H and
A3: fun f is linear ; :: thesis: f is Morphism of G,H
reconsider f9 = f as RingMorphism by A3, Def6;
dom f9 = G by A1;
then G <= H by A2, Def8;
then f9 is Morphism of G,H by A1, A2, Def9;
hence f is Morphism of G,H ; :: thesis: verum