theorem Th18: :: CAT_5:18

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