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 A1, Th4;

A4: Hom ((c opp),(b opp)) <> {} by A2, Th4;

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 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; :: thesis: verum

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 A1, Th4;

A4: Hom ((c opp),(b opp)) <> {} by A2, Th4;

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 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; :: thesis: verum