theorem Th27: :: CAT_5:27

for C being Category
for f being Morphism of C
for g being Element of Hom (dom f) holds f (*) g in Hom (cod f)