let R be Ring; for g, f being LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
defpred S1[ LModMorphism of R, LModMorphism of R] means dom $1 = cod $2;
let g, f be LModMorphism of R; ( dom g = cod f implies ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1:
S1[g,f]
; ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
consider G2, G3 being LeftMod of R such that
A2:
g is Morphism of G2,G3
by Th9;
A3:
G2 = dom g
by A2, Def8;
consider G1, G2 being LeftMod of R such that
A4:
f is Morphism of G1,G2
by Th9;
G2 = cod f
by A4, Def8;
hence
ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
by A1, A2, A3, A4; verum