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 = (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 = (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 = (f opp) * (g opp)

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds g * f = (f opp) * (g opp)

let g be Morphism of b,c; :: thesis: 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) ; :: thesis: verum

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; :: 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 = (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 = (f opp) * (g opp)

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds g * f = (f opp) * (g opp)

let g be Morphism of b,c; :: thesis: 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) ; :: thesis: verum