theorem Th7: :: ISOCAT_1:9

for A, B being Category
for F being Functor of A,B st F is one-to-one holds
Obj F is one-to-one