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

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