theorem Th65: :: OPPCAT_1:67

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