let I1, I2 be non empty set ; :: thesis: for J1 being non-Empty TopSpace-yielding ManySortedSet of I1

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds

product J1, product J2 are_homeomorphic

let J1 be non-Empty TopSpace-yielding ManySortedSet of I1; :: thesis: for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds

product J1, product J2 are_homeomorphic

let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; :: thesis: for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds

product J1, product J2 are_homeomorphic

let p be Function of I1,I2; :: thesis: ( p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) implies product J1, product J2 are_homeomorphic )

assume that

A1: p is bijective and

A2: for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ; :: thesis: product J1, product J2 are_homeomorphic

set H = the ProductHomeo of J1,J2,p;

the ProductHomeo of J1,J2,p is being_homeomorphism by A1, A2, Th78;

hence product J1, product J2 are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum

for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds

product J1, product J2 are_homeomorphic

let J1 be non-Empty TopSpace-yielding ManySortedSet of I1; :: thesis: for J2 being non-Empty TopSpace-yielding ManySortedSet of I2

for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds

product J1, product J2 are_homeomorphic

let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; :: thesis: for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds

product J1, product J2 are_homeomorphic

let p be Function of I1,I2; :: thesis: ( p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) implies product J1, product J2 are_homeomorphic )

assume that

A1: p is bijective and

A2: for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ; :: thesis: product J1, product J2 are_homeomorphic

set H = the ProductHomeo of J1,J2,p;

the ProductHomeo of J1,J2,p is being_homeomorphism by A1, A2, Th78;

hence product J1, product J2 are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum