theorem Th78: :: TOPS_5:78

for I1, I2 being 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
for H being ProductHomeo of J1,J2,p st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
H is being_homeomorphism