let R be Ring; for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
let V be LeftMod_DOMAIN of R; for g, f being Element of Morphs V st dom' g = cod' f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means dom' $1 = cod' $2;
let g, f be Element of Morphs V; ( dom' g = cod' f implies ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1:
S1[g,f]
; ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
consider G2, G3 being strict Element of V such that
A2:
g is strict Morphism of G2,G3
by Def7;
consider G1, G29 being strict Element of V such that
A3:
f is strict Morphism of G1,G29
by Def7;
A4:
G29 = cod' f
by A3, MOD_2:def 8;
G2 = dom' g
by A2, MOD_2:def 8;
hence
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
by A1, A2, A3, A4; verum