theorem Th8: :: MODCAT_1:8
for R being 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 )