theorem Th41: :: CAT_3:41

for I, x being set
for C being Category
for a being Object of C
for F being Projections_family of a,I st x in I holds
dom (F /. x) = a