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;

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 " = f " by A1, TOPS_2:def 4;

A4: the carrier of (InclPoset the topology of X) = the topology of X by YELLOW_1:1;

A5: 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 2;

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 " = f " by A1, TOPS_2:def 4;

A4: the carrier of (InclPoset the topology of X) = the topology of X by YELLOW_1:1;

A5: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;

now :: thesis: for x being Element of (oContMaps (X,Sierpinski_Space)) holds (alpha X) . x = (f ") . x

hence
alpha X is isomorphic
by A1, A3, FUNCT_2:63, WAYBEL_0:68; :: thesis: verumlet x be Element of (oContMaps (X,Sierpinski_Space)); :: thesis: (alpha X) . x = (f ") . x

reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2;

[#] Sierpinski_Space <> {} ;

then A6: g " A is open by TOPS_2:43;

then A7: g " A in the topology of X ;

A8: f . (g " A) = chi ((g " A), the carrier of X) by A2, A6

.= x by A5, FUNCT_3:40 ;

thus (alpha X) . x = g " A by Def4

.= (f ") . x by A1, A3, A4, A7, A8, FUNCT_2:26 ; :: thesis: verum

end;reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2;

[#] Sierpinski_Space <> {} ;

then A6: g " A is open by TOPS_2:43;

then A7: g " A in the topology of X ;

A8: f . (g " A) = chi ((g " A), the carrier of X) by A2, A6

.= x by A5, FUNCT_3:40 ;

thus (alpha X) . x = g " A by Def4

.= (f ") . x by A1, A3, A4, A7, A8, FUNCT_2:26 ; :: thesis: verum