deffunc H1( Function) -> set = \$1 " {1};
consider f being Function such that
A1: dom f = the carrier of () and
A2: for x being Element of () holds f . x = H1(x) from 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 () 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 (),(InclPoset the topology of X) by ;
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 () by WAYBEL26:2;
hence f . g = g " {1} by A2; :: thesis: verum