theorem Th3: :: ISOCAT_2:5

for A being Category
for f being Morphism of A holds (id (cod f)) (*) f = f