theorem Th17: :: CAT_5:17

for X being non empty categorial set
for Y being non empty set st ( for A, B, C being Element of X
for F being Functor of A,B
for G being Functor of B,C st F in Y & G in Y holds
G * F in Y ) & ( for A being Element of X holds id A in Y ) holds
ex C being strict Categorial Category st
( the carrier of C = X & ( for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C iff F in Y ) ) )