theorem Th4: :: ISOCAT_2:6

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