let X be non empty TopSpace; :: thesis: 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
A1:
f is isomorphic
and
A2:
for V being open Subset of X holds f . V = chi V,the carrier of X
by WAYBEL26:5;
A3:
( f is one-to-one & rng f = [#] (oContMaps X,Sierpinski_Space ) )
by A1, WAYBEL_0:66;
then A4:
f " = f "
by TOPS_2:def 4;
A5:
( the topology of Sierpinski_Space = {{} ,{1},{0 ,1}} & the carrier of Sierpinski_Space = {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 5;
A6:
the carrier of (InclPoset the topology of X) = the topology of X
by YELLOW_1:1;
now let x be
Element of
(oContMaps X,Sierpinski_Space );
:: thesis: (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:55;
then A8:
g " A in the
topology of
X
by PRE_TOPC:def 5;
A9:
f . (g " A) =
chi (g " A),the
carrier of
X
by A2, A7
.=
x
by A5, FUNCT_3:49
;
thus (alpha X) . x =
g " A
by Def4
.=
(f " ) . x
by A3, A4, A6, A8, A9, FUNCT_2:32
;
:: thesis: verum end;
then
alpha X = f "
by FUNCT_2:113;
then
(alpha X) " = f
by A3, TOPS_2:64;
hence
for V being open Subset of X holds ((alpha X) " ) . V = chi V,the carrier of X
by A2; :: thesis: verum