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 A1: ( dom f = G & cod f = H & fun f is linear ) ; :: thesis: f is Morphism of G,H
then reconsider f' = f as LModMorphism of R by Def10;
f' is Morphism of G,H by A1, Def11;
hence f is Morphism of G,H ; :: thesis: verum