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