let R be Ring; :: thesis: for G, H being LeftMod of R
for f being LModMorphismStr of R st dom f = G & cod f = H & fun f is linear holds
f is Morphism of G,H
let G, H be LeftMod of R; :: thesis: for f being LModMorphismStr of R st dom f = G & cod f = H & fun f is linear holds
f is Morphism of G,H
let f be LModMorphismStr of R; :: thesis: ( dom f = G & cod f = H & fun f is linear implies f is Morphism of G,H )
assume that
A1: ( dom f = G & cod f = H ) and
A2: fun f is linear ; :: thesis: f is Morphism of G,H
reconsider f9 = f as LModMorphism of R by A2, Def10;
f9 is Morphism of G,H by A1, Def11;
hence f is Morphism of G,H ; :: thesis: verum