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

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

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

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

consider G, H being LeftMod of R such that

A1: F is Morphism of G,H by Th9;

reconsider F9 = F as Morphism of G,H by A1;

consider f being Function of G,H such that

A2: ( LModMorphismStr(# the Dom of F9, the Cod of F9, the Fun of F9 #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by Th7;

take G ; :: thesis: ex H being LeftMod of R ex f being Function of G,H st

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

take H ; :: thesis: ex f being Function of G,H st

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

take f ; :: thesis: ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

thus ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by A2; :: thesis: verum

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

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

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

consider G, H being LeftMod of R such that

A1: F is Morphism of G,H by Th9;

reconsider F9 = F as Morphism of G,H by A1;

consider f being Function of G,H such that

A2: ( LModMorphismStr(# the Dom of F9, the Cod of F9, the Fun of F9 #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by Th7;

take G ; :: thesis: ex H being LeftMod of R ex f being Function of G,H st

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

take H ; :: thesis: ex f being Function of G,H st

( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

take f ; :: thesis: ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )

thus ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by A2; :: thesis: verum