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: H is being_homeomorphism

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

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: H is being_homeomorphism

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

hence
H is being_homeomorphism
by A5, Th48; :: thesis: verum
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 ) )

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

hence
H .: K = L
by FUNCT_2:def 10; :: thesis: verum
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 )

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 A16, WAYBEL18:def 2;

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

end;( 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

given V being Subset of (product J1) such that A16:
( V in K & H .: V = W )
; :: thesis: W in L
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 A1, FUNCT_2:def 3;

then consider i being object such that

A8: ( i in I1 & p . i = j ) by FUNCT_2:11;

A9: i in dom p by A8, FUNCT_2:def 1;

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 A8, PARTFUN1:def 2;

then product ((Carrier J1) +* (i,Vi)) c= product (Carrier J1) by A11, Th39;

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

reconsider f0 = f as one-to-one Function by A10;

rng f0 = [#] ((J2 * p) . i) by A10, TOPS_2:def 5

.= [#] (J2 . j) by A9, A8, FUNCT_1:13

.= 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;( 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 A1, FUNCT_2:def 3;

then consider i being object such that

A8: ( i in I1 & p . i = j ) by FUNCT_2:11;

A9: i in dom p by A8, FUNCT_2:def 1;

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 A8, PARTFUN1:def 2;

then product ((Carrier J1) +* (i,Vi)) c= product (Carrier J1) by A11, Th39;

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

hence
V in K
by A12, WAYBEL18:def 2; :: thesis: H .: V = W
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 A8, A9, FUNCT_1:13;

W0j in the topology of (J2 . j) by A6, PRE_TOPC:def 2;

then W1j in the topology of ((J2 * p) . i) by A8, A9, FUNCT_1:13;

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 A10, A14, TOPS_2:43; :: thesis: verum

end;( 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 A8, A9, FUNCT_1:13;

W0j in the topology of (J2 . j) by A6, PRE_TOPC:def 2;

then W1j in the topology of ((J2 * p) . i) by A8, A9, FUNCT_1:13;

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 A10, A14, TOPS_2:43; :: thesis: verum

reconsider f0 = f as one-to-one Function by A10;

rng f0 = [#] ((J2 * p) . i) by A10, TOPS_2:def 5

.= [#] (J2 . j) by A9, A8, FUNCT_1:13

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

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 A16, WAYBEL18:def 2;

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

hence
W in L
by A19, WAYBEL18:def 2; :: thesis: verum
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 A17, FUNCT_2:def 1;

then A21: (J2 * p) . i = J2 . j by FUNCT_1:13;

reconsider Wj = f .: Vi as Subset of (J2 . j) by a21, FUNCT_1:13;

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 A21, A17, A20, T_0TOPSP:def 2; :: 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;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 A17, FUNCT_2:def 1;

then A21: (J2 * p) . i = J2 . j by FUNCT_1:13;

reconsider Wj = f .: Vi as Subset of (J2 . j) by a21, FUNCT_1:13;

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 A21, A17, A20, T_0TOPSP:def 2; :: thesis: W = product ((Carrier J2) +* (j,Wj))

thus W = product ((Carrier J2) +* (j,Wj)) by A16, A1, A3, A4, A18, A20, Th76; :: thesis: verum