let X be non empty TopSpace; :: thesis: for n being Nat
for p being Point of ()
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )

let n be Nat; :: thesis: for p being Point of ()
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )

let p be Point of (); :: thesis: for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )

let f be Function of X,R^1; :: thesis: ( f is continuous implies ex g being Function of X,() st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous ) )

assume A1: f is continuous ; :: thesis: ex g being Function of X,() st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )

defpred S1[ set , set ] means \$2 = (f . \$1) * p;
A2: for x being Element of X ex y being Element of () st S1[x,y] ;
ex g being Function of the carrier of X, the carrier of () st
for x being Element of X holds S1[x,g . x] from then consider g being Function of the carrier of X, the carrier of () such that
A3: for x being Element of X holds S1[x,g . x] ;
reconsider g = g as Function of X,() ;
for r0 being Point of X
for V being Subset of () st g . r0 in V & V is open holds
ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )
proof
let r0 be Point of X; :: thesis: for V being Subset of () st g . r0 in V & V is open holds
ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )

let V be Subset of (); :: thesis: ( g . r0 in V & V is open implies ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) )

assume that
A4: g . r0 in V and
A5: V is open ; :: thesis: ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )

A6: g . r0 in Int V by ;
reconsider u = g . r0 as Point of () by TOPREAL3:8;
consider s being Real such that
A7: s > 0 and
A8: Ball (u,s) c= V by ;
now :: thesis: ( ( p <> 0. () & ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) ) or ( p = 0. () & ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) ) )
per cases ( p <> 0. () or p = 0. () ) ;
case A9: p <> 0. () ; :: thesis: ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )

then A10: |.p.| <> 0 by TOPRNS_1:24;
set r2 = s / |.p.|;
reconsider G1 = ].((f . r0) - (s / |.p.|)),((f . r0) + (s / |.p.|)).[ as Subset of R^1 by TOPMETR:17;
A11: f . r0 < (f . r0) + (s / |.p.|) by ;
then (f . r0) - (s / |.p.|) < f . r0 by XREAL_1:19;
then A12: f . r0 in G1 by ;
G1 is open by JORDAN6:35;
then consider W2 being Subset of X such that
A13: r0 in W2 and
A14: W2 is open and
A15: f .: W2 c= G1 by ;
g .: W2 c= V
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: W2 or y in V )
assume y in g .: W2 ; :: thesis: y in V
then consider r being object such that
A16: r in dom g and
A17: r in W2 and
A18: y = g . r by FUNCT_1:def 6;
reconsider r = r as Point of X by A16;
dom f = the carrier of X by FUNCT_2:def 1;
then f . r in f .: W2 by ;
then A19: |.((f . r) - (f . r0)).| < s / |.p.| by ;
reconsider t = f . r, t0 = f . r0 as Real ;
A20: |.(t0 - t).| = |.(t - t0).| by UNIFORM1:11;
reconsider v = g . r as Point of () by TOPREAL3:8;
g . r0 = (f . r0) * p by A3;
then A21: |.((g . r0) - (g . r)).| = |.(((f . r0) * p) - ((f . r) * p)).| by A3
.= |.(((f . r0) - (f . r)) * p).| by RLVECT_1:35
.= |.(t0 - t).| * |.p.| by TOPRNS_1:7 ;
|.((f . r) - (f . r0)).| * |.p.| < (s / |.p.|) * |.p.| by ;
then |.((g . r0) - (g . r)).| < s by ;
then dist (u,v) < s by JGRAPH_1:28;
then g . r in Ball (u,s) by METRIC_1:11;
hence y in V by ; :: thesis: verum
end;
hence ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) by ; :: thesis: verum
end;
case A22: p = 0. () ; :: thesis: ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )

A23: for r being Point of X holds g . r = 0. ()
proof
let r be Point of X; :: thesis: g . r = 0. ()
thus g . r = (f . r) * p by A3
.= 0. () by ; :: thesis: verum
end;
then A24: 0. () in V by A4;
set W2 = [#] X;
g .: ([#] X) c= V
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: ([#] X) or y in V )
assume y in g .: ([#] X) ; :: thesis: y in V
then ex x being object st
( x in dom g & x in [#] X & y = g . x ) by FUNCT_1:def 6;
hence y in V by ; :: thesis: verum
end;
hence ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) ; :: thesis: verum
end;
end;
end;
hence ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) ; :: thesis: verum
end;
then g is continuous by JGRAPH_2:10;
hence ex g being Function of X,() st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous ) by A3; :: thesis: verum