let C be Category; for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
let a, b, c be Object of C; for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
let f be Morphism of a,b; for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
let g be Morphism of b,c; ( Hom (a,b) <> {} & Hom (b,c) <> {} implies (g * f) opp = (f opp) (*) (g opp) )
assume A1:
( Hom (a,b) <> {} & Hom (b,c) <> {} )
; (g * f) opp = (f opp) (*) (g opp)
A2:
Hom (a,c) <> {}
by A1, CAT_1:24;
thus (g * f) opp =
g * f
by A2, Def6
.=
(g (*) f) opp
by A1, CAT_1:def 13
.=
(f opp) (*) (g opp)
by A1, Th14
; verum