let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds product J,J . i are_homeomorphic
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I holds product J,J . i are_homeomorphic
let i be Element of I; :: thesis: product J,J . i are_homeomorphic
proj (J,i) is being_homeomorphism by Th67;
hence product J,J . i are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum