let T be T_0-TopSpace; :: thesis: ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
take M = the carrier of (InclPoset the topology of T); :: thesis: ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
set J = M --> Sierpinski_Space;
reconsider PP = { (product ((Carrier (M --> Sierpinski_Space)) +* (m,{1}))) where m is Element of M : verum } as prebasis of (product (M --> Sierpinski_Space)) by Th13;
deffunc H₁( object ) -> Element of K19(K20( the topology of T,{0,1})) = chi ( { u where u is Subset of T : ( $1 in u & u is open ) } , the topology of T);
consider f being Function such that
A1: dom f = the carrier of T and
A2: for x being object st x in the carrier of T holds
f . x = H₁(x) from FUNCT_1:sch 3();
rng f c= the carrier of (product (M --> Sierpinski_Space))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of (product (M --> Sierpinski_Space)) )
assume y in rng f ; :: thesis: y in the carrier of (product (M --> Sierpinski_Space))
then consider x being object such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
set ch = chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T);
A4: dom (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) = the topology of T by FUNCT_3:def 3
.= M by YELLOW_1:1
.= dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def 2 ;
A5: for z being object st z in dom (Carrier (M --> Sierpinski_Space)) holds
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z

proof

let z be object ; :: thesis: ( z in dom (Carrier (M --> Sierpinski_Space)) implies (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z )
assume z in dom (Carrier (M --> Sierpinski_Space)) ; :: thesis: (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z
then A6: z in M ;
then z in the topology of T by YELLOW_1:1;
then z in dom (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) by FUNCT_3:def 3;
then A7: (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . z in rng (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) by FUNCT_1:def 3;
ex R being 1-sorted st
( R = (M --> Sierpinski_Space) . z & (Carrier (M --> Sierpinski_Space)) . z = the carrier of R ) by A6, PRALG_1:def 15;
then (Carrier (M --> Sierpinski_Space)) . z = the carrier of Sierpinski_Space by A6, FUNCOP_1:7
.= {0,1} by Def9 ;
hence (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z by A7; :: thesis: verum

end;

y = chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T) by A1, A2, A3;
then y in product (Carrier (M --> Sierpinski_Space)) by A4, A5, CARD_3:def 5;
hence y in the carrier of (product (M --> Sierpinski_Space)) by Def3; :: thesis: verum

end;

then reconsider f = f as Function of T,(product (M --> Sierpinski_Space)) by A1, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: corestr f is being_homeomorphism
A8: rng (corestr f) = [#] (Image f) by FUNCT_2:def 3;
for A being Subset of (product (M --> Sierpinski_Space)) st A in PP holds
f " A is open

proof

{1} c= {0,1} by ZFMISC_1:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
let A be Subset of (product (M --> Sierpinski_Space)); :: thesis: ( A in PP implies f " A is open )
reconsider a = A as Subset of (product (Carrier (M --> Sierpinski_Space))) by Def3;
assume A in PP ; :: thesis: f " A is open
then consider i being Element of M such that
A9: a = product ((Carrier (M --> Sierpinski_Space)) +* (i,{1})) ;
A10: i in M ;
then A11: i in the topology of T by YELLOW_1:1;
then reconsider i9 = i as Subset of T ;
A12: i in dom (Carrier (M --> Sierpinski_Space)) by A10, PARTFUN1:def 2;
A13: i c= f " A

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in i or z in f " A )
assume A14: z in i ; :: thesis: z in f " A
set W = { u where u is Subset of T : ( z in u & u is open ) } ;
i9 is open by A11;
then A15: i in { u where u is Subset of T : ( z in u & u is open ) } by A14;
A16: for w being object st w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) holds
(chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w

proof

let w be object ; :: thesis: ( w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) implies (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w )
assume w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) ; :: thesis: (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
then w in dom (Carrier (M --> Sierpinski_Space)) by FUNCT_7:30;
then A17: w in M ;
then w in the topology of T by YELLOW_1:1;
then A18: w in dom (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) by FUNCT_3:def 3;

per cases ( w = i or w <> i ) ;

suppose w = i ; :: thesis: (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w

then ( ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w = {1} & (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w = 1 ) by A11, A12, A15, FUNCT_3:def 3, FUNCT_7:31;
hence (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w by TARSKI:def 1; :: thesis: verum

end;

suppose A19: w <> i ; :: thesis: (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w

A20: (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in rng (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) by A18, FUNCT_1:def 3;
ex r being 1-sorted st
( r = (M --> Sierpinski_Space) . w & (Carrier (M --> Sierpinski_Space)) . w = the carrier of r ) by A17, PRALG_1:def 15;
then A21: (Carrier (M --> Sierpinski_Space)) . w = the carrier of Sierpinski_Space by A17, FUNCOP_1:7
.= {0,1} by Def9 ;
((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w = (Carrier (M --> Sierpinski_Space)) . w by A19, FUNCT_7:32;
hence (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w by A21, A20; :: thesis: verum

end;

end;

end;

A22: dom (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) = the topology of T by FUNCT_3:def 3
.= M by YELLOW_1:1
.= dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def 2
.= dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) by FUNCT_7:30 ;
A23: z in i9 by A14;
then f . z = chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T) by A2;
then f . z in A by A9, A22, A16, CARD_3:def 5;
hence z in f " A by A1, A23, FUNCT_1:def 7; :: thesis: verum

end;

A24: ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . i = {1} by A12, FUNCT_7:31;
f " A c= i

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f " A or z in i )
set W = { u where u is Subset of T : ( z in u & u is open ) } ;
assume z in f " A ; :: thesis: z in i
then ( f . z in a & f . z = chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T) ) by A2, FUNCT_1:def 7;
then consider g being Function such that
A25: chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T) = g and
dom g = dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) and
A26: for w being object st w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) holds
g . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w by A9, CARD_3:def 5;
i in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) by A12, FUNCT_7:30;
then g . i in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . i by A26;
then (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . i = 1 by A24, A25, TARSKI:def 1;
then i in { u where u is Subset of T : ( z in u & u is open ) } by FUNCT_3:36;
then ex uu being Subset of T st
( i = uu & z in uu & uu is open ) ;
hence z in i ; :: thesis: verum

end;

then f " A = i by A13;
hence f " A is open by A11; :: thesis: verum

end;

then f is continuous by YELLOW_9:36;
then A27: ( dom (corestr f) = [#] T & corestr f is continuous ) by Th10, FUNCT_2:def 1;
A28: corestr f is one-to-one

proof

let x, y be Element of T; :: according to WAYBEL_1:def 1 :: thesis: ( not (corestr f) . x = (corestr f) . y or x = y )
set U1 = { u where u is Subset of T : ( x in u & u is open ) } ;
set U2 = { u where u is Subset of T : ( y in u & u is open ) } ;
assume A29: (corestr f) . x = (corestr f) . y ; :: thesis: x = y
thus x = y :: thesis: verum

proof

A30: ( f . x = chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T) & f . y = chi ( { u where u is Subset of T : ( y in u & u is open ) } , the topology of T) ) by A2;
assume not x = y ; :: thesis: contradiction
then consider V being Subset of T such that
A31: V is open and
A32: ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by T_0TOPSP:def 7;
A33: V in the topology of T by A31;

per cases ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by A32;

suppose A34: ( x in V & not y in V ) ; :: thesis: contradiction

reconsider v = V as Subset of T ;
A35: not v in { u where u is Subset of T : ( y in u & u is open ) }

proof

assume v in { u where u is Subset of T : ( y in u & u is open ) } ; :: thesis: contradiction
then ex u being Subset of T st
( u = v & y in u & u is open ) ;
hence contradiction by A34; :: thesis: verum

end;

v in { u where u is Subset of T : ( x in u & u is open ) } by A31, A34;
then (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . v = 1 by A33, FUNCT_3:def 3;
hence contradiction by A29, A30, A33, A35, FUNCT_3:def 3; :: thesis: verum

end;

suppose A36: ( y in V & not x in V ) ; :: thesis: contradiction

reconsider v = V as Subset of T ;
A37: not v in { u where u is Subset of T : ( x in u & u is open ) }

proof

assume v in { u where u is Subset of T : ( x in u & u is open ) } ; :: thesis: contradiction
then ex u being Subset of T st
( u = v & x in u & u is open ) ;
hence contradiction by A36; :: thesis: verum

end;

v in { u where u is Subset of T : ( y in u & u is open ) } by A31, A36;
then (chi ( { u where u is Subset of T : ( y in u & u is open ) } , the topology of T)) . v = 1 by A33, FUNCT_3:def 3;
hence contradiction by A29, A30, A33, A37, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

end;

A38: for V being Subset of T st V is open holds
f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)

proof

let V be Subset of T; :: thesis: ( V is open implies f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) )
assume A39: V is open ; :: thesis: f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) c= f .: V

let y be object ; :: thesis: ( y in f .: V implies y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) )
assume y in f .: V ; :: thesis: y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)
then consider x being object such that
A40: x in dom f and
A41: x in V and
A42: y = f . x by FUNCT_1:def 6;
y in rng f by A40, A42, FUNCT_1:def 3;
then A43: y in the carrier of (Image f) by Th9;
set Q = { u where u is Subset of T : ( x in u & u is open ) } ;
A44: V in { u where u is Subset of T : ( x in u & u is open ) } by A39, A41;
A45: for W being object st W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) holds
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W

proof

let W be object ; :: thesis: ( W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) implies (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W )
assume W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) ; :: thesis: (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
then A46: W in dom (Carrier (M --> Sierpinski_Space)) by FUNCT_7:30;
then A47: W in M ;
then A48: W in the topology of T by YELLOW_1:1;
then A49: W in dom (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) by FUNCT_3:def 3;

per cases ( W = V or W <> V ) ;

suppose W = V ; :: thesis: (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W

then ( ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W = {1} & (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W = 1 ) by A44, A46, A48, FUNCT_3:def 3, FUNCT_7:31;
hence (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W by TARSKI:def 1; :: thesis: verum

end;

suppose A50: W <> V ; :: thesis: (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W

A51: (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in rng (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) by A49, FUNCT_1:def 3;
ex r being 1-sorted st
( r = (M --> Sierpinski_Space) . W & (Carrier (M --> Sierpinski_Space)) . W = the carrier of r ) by A47, PRALG_1:def 15;
then A52: (Carrier (M --> Sierpinski_Space)) . W = the carrier of Sierpinski_Space by A47, FUNCOP_1:7
.= {0,1} by Def9 ;
((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W = (Carrier (M --> Sierpinski_Space)) . W by A50, FUNCT_7:32;
hence (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W by A52, A51; :: thesis: verum

end;

end;

end;

A53: dom (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) = the topology of T by FUNCT_3:def 3
.= M by YELLOW_1:1
.= dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def 2
.= dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by FUNCT_7:30 ;
y = chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T) by A2, A40, A42;
then y in product ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by A53, A45, CARD_3:def 5;
hence y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) by A43, XBOOLE_0:def 4; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) or y in f .: V )
assume A54: y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) ; :: thesis: y in f .: V
then y in product ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by XBOOLE_0:def 4;
then consider g being Function such that
A55: y = g and
dom g = dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) and
A56: for W being object st W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) holds
g . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W by CARD_3:def 5;
rng f = the carrier of (Image f) by Th9;
then y in rng f by A54, XBOOLE_0:def 4;
then consider x being object such that
A57: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
V in the topology of T by A39;
then V in M by YELLOW_1:1;
then A58: V in dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def 2;
then V in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by FUNCT_7:30;
then g . V in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . V by A56;
then A59: g . V in {1} by A58, FUNCT_7:31;
set Q = { u where u is Subset of T : ( x in u & u is open ) } ;
y = chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T) by A2, A57;
then (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . V = 1 by A55, A59, TARSKI:def 1;
then V in { u where u is Subset of T : ( x in u & u is open ) } by FUNCT_3:36;
then ex u being Subset of T st
( u = V & x in u & u is open ) ;
hence y in f .: V by A57, FUNCT_1:def 6; :: thesis: verum

end;

A60: for V being Subset of T st V is open holds
((corestr f) ") " V is open

proof

let V be Subset of T; :: thesis: ( V is open implies ((corestr f) ") " V is open )
A61: PP c= the topology of (product (M --> Sierpinski_Space)) by TOPS_2:64;
assume A62: V is open ; :: thesis: ((corestr f) ") " V is open
then V in the topology of T ;
then reconsider W = V as Element of M by YELLOW_1:1;
A63: product ((Carrier (M --> Sierpinski_Space)) +* (W,{1})) in PP ;
then reconsider Q = product ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) as Subset of (product (M --> Sierpinski_Space)) ;
(corestr f) .: V = Q /\ ([#] (Image f)) by A38, A62;
then (corestr f) .: V in the topology of (Image f) by A63, A61, PRE_TOPC:def 4;
then (corestr f) .: V is open ;
hence ((corestr f) ") " V is open by A8, A28, TOPS_2:54; :: thesis: verum

end;

[#] T <> {} ;
then (corestr f) " is continuous by A60, TOPS_2:43;
hence corestr f is being_homeomorphism by A8, A28, A27, TOPS_2:def 5; :: thesis: verum