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