let C be Category; for f, g being Morphism of (C opp) st dom g = cod f holds
opp (g (*) f) = (opp f) (*) (opp g)
let f, g be Morphism of (C opp); ( dom g = cod f implies opp (g (*) f) = (opp f) (*) (opp g) )
assume A1:
dom g = cod f
; opp (g (*) f) = (opp f) (*) (opp g)
A2:
( cod (opp g) = dom g & dom (opp f) = cod f )
;
then A3:
[(opp f),(opp g)] in dom the Comp of C
by A1, CAT_1:15;
thus opp (g (*) f) =
(~ the Comp of C) . ((opp g),(opp f))
by A1, CAT_1:16
.=
the Comp of C . ((opp f),(opp g))
by A3, FUNCT_4:def 2
.=
(opp f) (*) (opp g)
by A1, A2, CAT_1:16
; verum