let R be Ring; 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; 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
; 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
; 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
; ( 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; verum