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; :: thesis: for V being open Subset of X holds (() ") . V = chi (V, the carrier of X)
consider f being Function of (InclPoset the topology of X),() 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 = [#] () by ;
A6: f " = f " by ;
now :: thesis: for x being Element of () holds () . x = (f ") . x
let x be Element of (); :: thesis: () . x = (f ") . x
reconsider 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 ;
thus () . x = g " A by Def4
.= (f ") . x by A2, A6, A4, A8, A9, FUNCT_2:26 ; :: thesis: verum
end;
then alpha X = f " by FUNCT_2:63;
then (alpha X) " = f by ;
hence for V being open Subset of X holds (() ") . V = chi (V, the carrier of X) by A3; :: thesis: verum