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 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 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: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