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 = (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 = (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 = (f opp) * (g opp)
let f be Morphism of a,b; for g being Morphism of b,c holds g * f = (f opp) * (g opp)
let g be Morphism of b,c; g * f = (f opp) * (g opp)
reconsider f1 = f as Morphism of C ;
reconsider g1 = g as Morphism of C ;
A3:
Hom ((b opp),(a opp)) <> {}
by A1, Th4;
A4:
Hom ((c opp),(b opp)) <> {}
by A2, Th4;
g * f =
(g (*) f) opp
by A1, A2, CAT_1:def 13
.=
(f opp) (*) (g opp)
by A1, A2, Th14
.=
(f opp) * (g opp)
by A3, A4, CAT_1:def 13
;
hence
g * f = (f opp) * (g opp)
; verum