let R be Ring; :: thesis: for G, H being LeftMod of R

for f being Function of G,H st f is additive & f is homogeneous holds

LModMorphismStr(# G,H,f #) is strict Morphism of G,H

let G, H be LeftMod of R; :: thesis: for f being Function of G,H st f is additive & f is homogeneous holds

LModMorphismStr(# G,H,f #) is strict Morphism of G,H

let f be Function of G,H; :: thesis: ( f is additive & f is homogeneous implies LModMorphismStr(# G,H,f #) is strict Morphism of G,H )

assume A1: ( f is additive & f is homogeneous ) ; :: thesis: LModMorphismStr(# G,H,f #) is strict Morphism of G,H

set F = LModMorphismStr(# G,H,f #);

fun LModMorphismStr(# G,H,f #) = f ;

hence LModMorphismStr(# G,H,f #) is strict Morphism of G,H by A1, Th5; :: thesis: verum

for f being Function of G,H st f is additive & f is homogeneous holds

LModMorphismStr(# G,H,f #) is strict Morphism of G,H

let G, H be LeftMod of R; :: thesis: for f being Function of G,H st f is additive & f is homogeneous holds

LModMorphismStr(# G,H,f #) is strict Morphism of G,H

let f be Function of G,H; :: thesis: ( f is additive & f is homogeneous implies LModMorphismStr(# G,H,f #) is strict Morphism of G,H )

assume A1: ( f is additive & f is homogeneous ) ; :: thesis: LModMorphismStr(# G,H,f #) is strict Morphism of G,H

set F = LModMorphismStr(# G,H,f #);

fun LModMorphismStr(# G,H,f #) = f ;

hence LModMorphismStr(# G,H,f #) is strict Morphism of G,H by A1, Th5; :: thesis: verum