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

for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)

let G, H be LeftMod of R; :: thesis: for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)

let F be strict Morphism of G,H; :: thesis: ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)

consider f being Function of G,H such that

A1: LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) and

( f is additive & f is homogeneous ) by Th7;

take f ; :: thesis: F = LModMorphismStr(# G,H,f #)

thus F = LModMorphismStr(# G,H,f #) by A1; :: thesis: verum

for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)

let G, H be LeftMod of R; :: thesis: for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)

let F be strict Morphism of G,H; :: thesis: ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)

consider f being Function of G,H such that

A1: LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) and

( f is additive & f is homogeneous ) by Th7;

take f ; :: thesis: F = LModMorphismStr(# G,H,f #)

thus F = LModMorphismStr(# G,H,f #) by A1; :: thesis: verum