theorem Th22: :: CAT_7:22
for C being composable with_identities CategoryStr
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
Hom (a,c) <> {}