deffunc H_{1}( Function) -> set = $1 " {1};

consider f being Function such that

A1: dom f = the carrier of (oContMaps (X,Sierpinski_Space)) and

A2: for x being Element of (oContMaps (X,Sierpinski_Space)) holds f . x = H_{1}(x)
from FUNCT_1:sch 4();

rng f c= the topology of X

then reconsider f = f as Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) by A1, FUNCT_2:2;

take f ; :: thesis: for g being continuous Function of X,Sierpinski_Space holds f . g = g " {1}

let g be continuous Function of X,Sierpinski_Space; :: thesis: f . g = g " {1}

g is Element of (oContMaps (X,Sierpinski_Space)) by WAYBEL26:2;

hence f . g = g " {1} by A2; :: thesis: verum

consider f being Function such that

A1: dom f = the carrier of (oContMaps (X,Sierpinski_Space)) and

A2: for x being Element of (oContMaps (X,Sierpinski_Space)) holds f . x = H

rng f c= the topology of X

proof

then
rng f c= the carrier of (InclPoset the topology of X)
by YELLOW_1:1;
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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the topology of X )

assume y in rng f ; :: thesis: y in the topology of X

then consider x being object such that

A3: x in dom f and

A4: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of (oContMaps (X,Sierpinski_Space)) by A1, A3;

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

[#] Sierpinski_Space <> {} ;

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

y = g " A by A2, A4;

hence y in the topology of X by A5; :: thesis: verum

end;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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the topology of X )

assume y in rng f ; :: thesis: y in the topology of X

then consider x being object such that

A3: x in dom f and

A4: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of (oContMaps (X,Sierpinski_Space)) by A1, A3;

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

[#] Sierpinski_Space <> {} ;

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

y = g " A by A2, A4;

hence y in the topology of X by A5; :: thesis: verum

then reconsider f = f as Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) by A1, FUNCT_2:2;

take f ; :: thesis: for g being continuous Function of X,Sierpinski_Space holds f . g = g " {1}

let g be continuous Function of X,Sierpinski_Space; :: thesis: f . g = g " {1}

g is Element of (oContMaps (X,Sierpinski_Space)) by WAYBEL26:2;

hence f . g = g " {1} by A2; :: thesis: verum