let R be Ring; :: thesis: for F being LModMorphism of R ex G, H being LeftMod of R st F is Morphism of G,H

let F be LModMorphism of R; :: thesis: ex G, H being LeftMod of R st F is Morphism of G,H

take G = the Dom of F; :: thesis: ex H being LeftMod of R st F is Morphism of G,H

take H = the Cod of F; :: thesis: F is Morphism of G,H

( dom F = G & cod F = H ) ;

hence F is Morphism of G,H by Def8; :: thesis: verum

let F be LModMorphism of R; :: thesis: ex G, H being LeftMod of R st F is Morphism of G,H

take G = the Dom of F; :: thesis: ex H being LeftMod of R st F is Morphism of G,H

take H = the Cod of F; :: thesis: F is Morphism of G,H

( dom F = G & cod F = H ) ;

hence F is Morphism of G,H by Def8; :: thesis: verum