theorem Th11: :: ALTCAT_2:11

for C being Category
for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)