let C be Category; 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; ( 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) <> {}
; 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 A1, Th4;
A4:
Hom ((c opp),(b opp)) <> {}
by A2, Th4;
let f be Morphism of a,b; for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
let g be Morphism of b,c; (g (*) f) opp = (f opp) (*) (g opp)
A5: dom g =
b
by A2, CAT_1:5
.=
cod f
by A1, CAT_1:5
;
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 A2, CAT_1:5
.=
cod (g opp)
by A4, CAT_1:5
;
A9: cod f =
b opp
by A1, CAT_1:5
.=
dom (f opp)
by A3, CAT_1:5
;
then
( the Comp of C = ~ the Comp of (C opp) & [(f opp),(g opp)] in dom the Comp of (C opp) )
by A5, A8, CAT_1:15, FUNCT_4:53;
then
the Comp of C . (g,f) = the Comp of (C opp) . ((f opp),(g opp))
by A7, FUNCT_4:def 2;
hence
(g (*) f) opp = (f opp) (*) (g opp)
by A5, A6, A8, A9, CAT_1:16; verum