theorem Th3: :: CAT_6:3

for C being CategoryStr
for f1, f2 being morphism of C
for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 & f1 |> f2 holds
f1 (*) f2 = g2 (*) g1