theorem Th53: :: TOPS_5:53

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