theorem Th44: :: OPPCAT_1:46

for C, D being Category
for F being Function of the carrier' of C, the carrier' of D
for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp