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