theorem Th62: :: CAT_3:62

for I, x being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st x in I holds
cod (F /. x) = c