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

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