set c = the carrier of S;
reconsider f = the carrier of S --> (In (0,REAL)) as RealMap of S ;
take f ; :: thesis: f is continuous
A1: dom f = the carrier of S by FUNCT_2:def 1;
let Y be Subset of REAL; :: according to PSCOMP_1:def 3 :: thesis: ( Y is closed implies f " Y is closed )
A2: rng f = {0} by FUNCOP_1:8;
assume Y is closed ; :: thesis: f " Y is closed

per cases ( 0 in Y or not 0 in Y ) ;

suppose 0 in Y ; :: thesis: f " Y is closed

then A3: rng f c= Y by A2, ZFMISC_1:31;
f " Y = f " ((rng f) /\ Y) by RELAT_1:133
.= f " (rng f) by A3, XBOOLE_1:28
.= [#] S by A1, RELAT_1:134 ;
hence f " Y is closed ; :: thesis: verum

end;

suppose not 0 in Y ; :: thesis: f " Y is closed

then A4: rng f misses Y by A2, ZFMISC_1:50;
f " Y = f " ((rng f) /\ Y) by RELAT_1:133
.= f " {} by A4, XBOOLE_0:def 7
.= {} S ;
hence f " Y is closed ; :: thesis: verum

end;

end;