theorem :: CAT_1:15

for C being Category
for f, g being Morphism of C holds
( dom g = cod f iff [g,f] in dom the Comp of C ) by Def4;