theorem Th52: :: TOPS_5:52

for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds rng (proj (J,i)) = the carrier of (J . i)