let I1, I2 be non empty set ; 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; 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; 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; ( 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
; 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; verum