let C be Category; :: thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

let a, b, c be Object of C; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) )

assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

A3: Hom ((b opp),(a opp)) <> {} by ;
A4: Hom ((c opp),(b opp)) <> {} by ;
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
let g be Morphism of b,c; :: thesis: (g (*) f) opp = (f opp) (*) (g opp)
A5: dom g = b by
.= cod f by ;
then A6: g (*) f = the Comp of C . (g,f) by CAT_1:16;
A7: ( f opp = f & g opp = g ) by A1, A2, Def6;
A8: dom g = b opp by
.= cod (g opp) by ;
A9: cod f = b opp by
.= dom (f opp) by ;
then ( the Comp of C = ~ the Comp of (C opp) & [(f opp),(g opp)] in dom the Comp of (C opp) ) by ;
then the Comp of C . (g,f) = the Comp of (C opp) . ((f opp),(g opp)) by ;
hence (g (*) f) opp = (f opp) (*) (g opp) by A5, A6, A8, A9, CAT_1:16; :: thesis: verum