theorem Th63: :: OPPCAT_1:65

for C being Category
for f being Morphism of C holds (id* C) . f = f opp