let C be Category; :: thesis: for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} 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 ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} implies for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) )

assume ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) ; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

then ( Hom (a,b) <> {} & Hom (b,c) <> {} ) by Th4;

hence for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) by Th14; :: 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 ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} implies for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) )

assume ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) ; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)

then ( Hom (a,b) <> {} & Hom (b,c) <> {} ) by Th4;

hence for f being Morphism of a,b

for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) by Th14; :: thesis: verum