for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds product J,J . i are_homeomorphic