let R be Ring; :: thesis: for F being strict LModMorphism of R ex G, H being LeftMod of ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is linear )
let F be strict LModMorphism of R; :: thesis: ex G, H being LeftMod of ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is linear )
consider G, H being LeftMod of such that
A1: F is Morphism of G,H by Th16;
reconsider F' = F as Morphism of G,H by A1;
consider f being Function of G,H such that
A2: ( LModMorphismStr(# the Dom of F',the Cod of F',the Fun of F' #) = LModMorphismStr(# G,H,f #) & f is linear ) by Th14;
take G ; :: thesis: ex H being LeftMod of ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is linear )
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 linear )
take f ; :: thesis: ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is linear )
thus ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is linear ) by A2; :: thesis: verum