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
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

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
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

let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; :: thesis: 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

let p be Function of I1,I2; :: thesis: 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

let H be ProductHomeo of J1,J2,p; :: thesis: ( p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) implies H is being_homeomorphism )
assume that
A1: p is bijective and
A2: for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ; :: thesis:
consider F being ManySortedFunction of I1 such that
A3: for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) and
A4: for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) by A1, A2, Def5;
A5: H is bijective by A1, A2, Th77;
ex K being prebasis of (product J1) ex L being prebasis of (product J2) st H .: K = L
proof
reconsider K = product_prebasis J1 as prebasis of (product J1) by WAYBEL18:def 3;
reconsider L = product_prebasis J2 as prebasis of (product J2) by WAYBEL18:def 3;
take K ; :: thesis: ex L being prebasis of (product J2) st H .: K = L
take L ; :: thesis: H .: K = L
for W being Subset of (product J2) holds
( W in L iff ex V being Subset of (product J1) st
( V in K & H .: V = W ) )
proof
let W be Subset of (product J2); :: thesis: ( W in L iff ex V being Subset of (product J1) st
( V in K & H .: V = W ) )

thus ( W in L implies ex V being Subset of (product J1) st
( V in K & H .: V = W ) ) :: thesis: ( ex V being Subset of (product J1) st
( V in K & H .: V = W ) implies W in L )
proof
assume W in L ; :: thesis: ex V being Subset of (product J1) st
( V in K & H .: V = W )

then consider j being set , T being TopStruct , W0j being Subset of T such that
A6: ( j in I2 & W0j is open & T = J2 . j ) and
A7: W = product ((Carrier J2) +* (j,W0j)) by WAYBEL18:def 2;
reconsider j = j as Element of I2 by A6;
reconsider Wj = W0j as Subset of (J2 . j) by A6;
j in I2 ;
then j in rng p by ;
then consider i being object such that
A8: ( i in I1 & p . i = j ) by FUNCT_2:11;
A9: i in dom p by ;
reconsider i = i as Element of I1 by A8;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A10: ( F . i = f & f is being_homeomorphism ) by A3;
reconsider Vi = f " Wj as Subset of (J1 . i) ;
A11: the carrier of (J1 . i) = [#] (J1 . i) by STRUCT_0:def 3
.= (Carrier J1) . i by PENCIL_3:7 ;
i in dom (Carrier J1) by ;
then product ((Carrier J1) +* (i,Vi)) c= product (Carrier J1) by ;
then reconsider V = product ((Carrier J1) +* (i,Vi)) as Subset of (product J1) by WAYBEL18:def 3;
take V ; :: thesis: ( V in K & H .: V = W )
A12: V is Subset of (product (Carrier J1)) by WAYBEL18:def 3;
ex k being set ex S being TopStruct ex U being Subset of S st
( k in I1 & U is open & S = J1 . k & V = product ((Carrier J1) +* (k,U)) )
proof
take i ; :: thesis: ex S being TopStruct ex U being Subset of S st
( i in I1 & U is open & S = J1 . i & V = product ((Carrier J1) +* (i,U)) )

take J1 . i ; :: thesis: ex U being Subset of (J1 . i) st
( i in I1 & U is open & J1 . i = J1 . i & V = product ((Carrier J1) +* (i,U)) )

take Vi ; :: thesis: ( i in I1 & Vi is open & J1 . i = J1 . i & V = product ((Carrier J1) +* (i,Vi)) )
reconsider W1j = Wj as Subset of ((J2 * p) . i) by ;
W0j in the topology of (J2 . j) by ;
then W1j in the topology of ((J2 * p) . i) by ;
then A14: W1j is open by PRE_TOPC:def 2;
( [#] ((J2 * p) . i) = {} implies [#] (J1 . i) = {} ) ;
hence ( i in I1 & Vi is open & J1 . i = J1 . i & V = product ((Carrier J1) +* (i,Vi)) ) by ; :: thesis: verum
end;
hence V in K by ; :: thesis: H .: V = W
reconsider f0 = f as one-to-one Function by A10;
rng f0 = [#] ((J2 * p) . i) by
.= [#] (J2 . j) by
.= the carrier of (J2 . j) by STRUCT_0:def 3 ;
then f .: (f " Wj) = Wj by FUNCT_1:77;
hence H .: V = W by A1, A3, A4, A7, A8, Th76, A10; :: thesis: verum
end;
given V being Subset of (product J1) such that A16: ( V in K & H .: V = W ) ; :: thesis: W in L
consider i being set , S being TopStruct , Vi being Subset of S such that
A17: ( i in I1 & Vi is open & S = J1 . i ) and
A18: V = product ((Carrier J1) +* (i,Vi)) by ;
reconsider i = i as Element of I1 by A17;
reconsider Vi = Vi as Subset of (J1 . i) by A17;
A19: W is Subset of (product (Carrier J2)) by WAYBEL18:def 3;
ex j being set ex T being TopStruct ex U being Subset of T st
( j in I2 & U is open & T = J2 . j & W = product ((Carrier J2) +* (j,U)) )
proof
reconsider j = p . i as Element of I2 ;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A20: ( F . i = f & f is being_homeomorphism ) by A3;
a21: i in dom p by ;
then A21: (J2 * p) . i = J2 . j by FUNCT_1:13;
reconsider Wj = f .: Vi as Subset of (J2 . j) by ;
take j ; :: thesis: ex T being TopStruct ex U being Subset of T st
( j in I2 & U is open & T = J2 . j & W = product ((Carrier J2) +* (j,U)) )

take J2 . j ; :: thesis: ex U being Subset of (J2 . j) st
( j in I2 & U is open & J2 . j = J2 . j & W = product ((Carrier J2) +* (j,U)) )

take Wj ; :: thesis: ( j in I2 & Wj is open & J2 . j = J2 . j & W = product ((Carrier J2) +* (j,Wj)) )
thus ( j in I2 & Wj is open & J2 . j = J2 . j ) by ; :: thesis: W = product ((Carrier J2) +* (j,Wj))
thus W = product ((Carrier J2) +* (j,Wj)) by A16, A1, A3, A4, A18, A20, Th76; :: thesis: verum
end;
hence W in L by ; :: thesis: verum
end;
hence H .: K = L by FUNCT_2:def 10; :: thesis: verum
end;
hence H is being_homeomorphism by ; :: thesis: verum