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

for F being Morphism of G,H ex f being Function of G,H st

( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

let G, H be LeftMod of R; :: thesis: for F being Morphism of G,H ex f being Function of G,H st

( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

let F be Morphism of G,H; :: thesis: ex f being Function of G,H st

( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

A1: the Cod of F = cod F

.= H by Def8 ;

A2: the Dom of F = dom F

.= G by Def8 ;

then reconsider f = the Fun of F as Function of G,H by A1;

take f ; :: thesis: ( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

thus ( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by A2, A1, Th4; :: thesis: verum

for F being Morphism of G,H ex f being Function of G,H st

( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

let G, H be LeftMod of R; :: thesis: for F being Morphism of G,H ex f being Function of G,H st

( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

let F be Morphism of G,H; :: thesis: ex f being Function of G,H st

( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

A1: the Cod of F = cod F

.= H by Def8 ;

A2: the Dom of F = dom F

.= G by Def8 ;

then reconsider f = the Fun of F as Function of G,H by A1;

take f ; :: thesis: ( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

thus ( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by A2, A1, Th4; :: thesis: verum