theorem Th9: :: CAT_8:9

for C1, C2 being category
for F being Functor of C1,C2 st F is isomorphism holds
F is bijective