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

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