theorem :: CAT_1:24

for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
Hom (a,c) <> {} by Th19;