theorem :: CAT_3:70

for I being set
for C being Category
for f being Morphism of C
for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp