theorem Th5: :: CAT_3:5

for I being set
for C being Category
for f being Morphism of C holds cods (I --> f) = I --> (cod f)