theorem Th28: :: CAT_5:28
for C being Category
for f being Morphism of C
for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom