let C be Category; :: thesis: 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); :: thesis: ( dom g = cod f implies opp (g (*) f) = (opp f) (*) (opp g) )
assume A1: dom g = cod f ; :: thesis: 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 ; :: thesis: verum