:: deftheorem Def5 defines ProductHomeo TOPS_5:def 5 :
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 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
for b₆ being Function of (product J1),(product J2) holds
( b₆ is ProductHomeo of J1,J2,p iff ex F being ManySortedFunction of I1 st
( ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (b₆ . g) . (p . i) = (F . i) . (g . i) ) ) );