for C being Category
for f, g being Morphism of (C opp) st dom g = cod f holds
opp (g (*) f) = (opp f) (*) (opp g)