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