let I be 2 -element set ; :: thesis: 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; :: thesis: 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; :: thesis: ( i <> j implies product J,[:(J . i),(J . j):] are_homeomorphic )
assume A1: i <> j ; :: thesis: 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; :: thesis: verum