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 linear )
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 linear )
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 linear )
A1: the Cod of F = cod F
.= H by Def11 ;
A2: the Dom of F = dom F
.= G by Def11 ;
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 linear )
thus ( LModMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = LModMorphismStr(# G,H,f #) & f is linear ) by A2, A1, Th10; :: thesis: verum