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
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; 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; 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; 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; ( 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
; 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
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
;
ex L being prebasis of (product J2) st H .: K = L
take
L
;
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);
( 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 ) )
( ex V being Subset of (product J1) st
( V in K & H .: V = W ) implies W in L )proof
assume
W in L
;
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
;
( 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
;
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
;
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
;
( 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;
verum
end;
hence
V in K
by A12, WAYBEL18:def 2;
H .: V = W
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;
verum
end;
given V being
Subset of
(product J1) such that A16:
(
V in K &
H .: V = W )
;
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)) )
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 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
;
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
;
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
;
( 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;
W = product ((Carrier J2) +* (j,Wj))
thus
W = product ((Carrier J2) +* (j,Wj))
by A16, A1, A3, A4, A18, A20, Th76;
verum
end;
hence
W in L
by A19, WAYBEL18:def 2;
verum
end;
hence
H .: K = L
by FUNCT_2:def 10;
verum
end;
hence
H is being_homeomorphism
by A5, Th48; verum