let I be 2 -element set ; for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I st i <> j holds
product J,[:(J . i),(J . j):] are_homeomorphic
let J be non-Empty TopSpace-yielding ManySortedSet of I; for i, j being Element of I st i <> j holds
product J,[:(J . i),(J . j):] are_homeomorphic
let i, j be Element of I; ( i <> j implies product J,[:(J . i),(J . j):] are_homeomorphic )
assume A1:
i <> j
; product J,[:(J . i),(J . j):] are_homeomorphic
reconsider f = <:(proj (J,i)),(proj (J,j)):> as Function of (product J),[:(J . i),(J . j):] by BORSUK_1:def 2;
f is being_homeomorphism
by A1, Th74;
hence
product J,[:(J . i),(J . j):] are_homeomorphic
by T_0TOPSP:def 1; verum