let C be Category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies (g * f) opp = (f opp) (*) (g opp) )

assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: (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 ; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies (g * f) opp = (f opp) (*) (g opp) )

assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: (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 ; :: thesis: verum