A1:
the carrier of Sierpinski_Space = {0,1}
by WAYBEL18:def 9;
the topology of Sierpinski_Space = {{},{1},{0,1}}
by WAYBEL18:def 9;
then
{1} in the topology of Sierpinski_Space
by ENUMSET1:def 1;
then reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def 2;
let X be non empty TopSpace; for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X)
consider f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) such that
A2:
f is isomorphic
and
A3:
for V being open Subset of X holds f . V = chi (V, the carrier of X)
by WAYBEL26:5;
A4:
the carrier of (InclPoset the topology of X) = the topology of X
by YELLOW_1:1;
A5:
rng f = [#] (oContMaps (X,Sierpinski_Space))
by A2, WAYBEL_0:66;
A6:
f " = f "
by A2, TOPS_2:def 4;
now for x being Element of (oContMaps (X,Sierpinski_Space)) holds (alpha X) . x = (f ") . xlet x be
Element of
(oContMaps (X,Sierpinski_Space));
(alpha X) . x = (f ") . xreconsider g =
x as
continuous Function of
X,
Sierpinski_Space by WAYBEL26:2;
[#] Sierpinski_Space <> {}
;
then A7:
g " A is
open
by TOPS_2:43;
then A8:
g " A in the
topology of
X
;
A9:
f . (g " A) =
chi (
(g " A), the
carrier of
X)
by A3, A7
.=
x
by A1, FUNCT_3:40
;
thus (alpha X) . x =
g " A
by Def4
.=
(f ") . x
by A2, A6, A4, A8, A9, FUNCT_2:26
;
verum end;
then
alpha X = f "
by FUNCT_2:63;
then
(alpha X) " = f
by A2, A5, TOPS_2:51;
hence
for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X)
by A3; verum