deffunc H₁( 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₁(x) from FUNCT_1:sch 4();
rng f c= the topology of X

proof

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 5;
let y be set ; :: 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 set such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 5;
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:55;
y = g " A by A2, A4;
hence y in the topology of X by A5, PRE_TOPC:def 5; :: thesis: verum

end;

then rng f c= the carrier of (InclPoset the topology of X) by YELLOW_1:1;
then reconsider f = f as Function of (oContMaps X,Sierpinski_Space ),(InclPoset the topology of X) by A1, FUNCT_2:4;
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