for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for p being Permutation of I holds product J, product (J * p) are_homeomorphic