let X be non empty TopSpace; :: thesis: for a being Real ex g being Function of X,R^1 st
( ( for p being Point of X holds g . p = a ) & g is continuous )
let a be Real; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X holds g . p = a ) & g is continuous )
reconsider a1 = a as Element of R^1 by TOPMETR:17, XREAL_0:def 1;
set g1 = the carrier of X --> a1;
reconsider g0 = the carrier of X --> a1 as Function of X,R^1 ;
for p being Point of X
for V being Subset of R^1 st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

proof

set f1 = g0;
let p be Point of X; :: thesis: for V being Subset of R^1 st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
let V be Subset of R^1; :: thesis: ( g0 . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) )
assume that
A1: g0 . p in V and
V is open ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
set G1 = V;
g0 .: ([#] X) c= V

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g0 .: ([#] X) or y in V )
assume y in g0 .: ([#] X) ; :: thesis: y in V
then ex x being object st
( x in dom g0 & x in [#] X & y = g0 . x ) by FUNCT_1:def 6;
then y = a by FUNCOP_1:7;
hence y in V by A1, FUNCOP_1:7; :: thesis: verum

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ; :: thesis: verum

end;

then ( ( for p being Point of X holds ( the carrier of X --> a1) . p = a ) & g0 is continuous ) by Th10, FUNCOP_1:7;
hence ex g being Function of X,R^1 st
( ( for p being Point of X holds g . p = a ) & g is continuous ) ; :: thesis: verum