let R be Ring; :: thesis: 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 S_{1}[ LModMorphism of R, LModMorphism of R] means dom $1 = cod $2;

let g, f be LModMorphism of R; :: thesis: ( 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: S_{1}[g,f]
; :: thesis: 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; :: thesis: verum

ex G1, G2, G3 being LeftMod of R st

( g is Morphism of G2,G3 & f is Morphism of G1,G2 )

defpred S

let g, f be LModMorphism of R; :: thesis: ( 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: S

( 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; :: thesis: verum