let X be non empty TopSpace; :: thesis: for n being Element of NAT
for p being Point of (TOP-REAL n)
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )
let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL n)
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )
let p be Point of (TOP-REAL n); :: thesis: for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) 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,(TOP-REAL n) 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,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )
defpred S₁[ set , set ] means $2 = (f . $1) * p;
A2: for x being Element of X ex y being Element of (TOP-REAL n) st S₁[x,y] ;
ex g being Function of the carrier of X,the carrier of (TOP-REAL n) st
for x being Element of X holds S₁[x,g . x] from FUNCT_2:sch 3(A2);
then consider g being Function of the carrier of X,the carrier of (TOP-REAL n) such that
A3: for x being Element of X holds S₁[x,g . x] ;
reconsider g = g as Function of X,(TOP-REAL n) ;
for r0 being Point of X
for V being Subset of (TOP-REAL n) 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 (TOP-REAL n) 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 (TOP-REAL n); :: 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 A4: ( g . r0 in V & V is open ) ; :: thesis: ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )
then A5: g . r0 in Int V by TOPS_1:55;
reconsider u = g . r0 as Point of (Euclid n) by TOPREAL3:13;
consider s being real number such that
A6: ( s > 0 & Ball u,s c= V ) by A5, GOBOARD6:8;

now

per cases ( p <> 0. (TOP-REAL n) or p = 0. (TOP-REAL n) ) ;

case A7: p <> 0. (TOP-REAL n) ; :: thesis: ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )

then A8: |.p.| <> 0 by TOPRNS_1:25;
set r2 = s / |.p.|;
reconsider G1 = ].((f . r0) - (s / |.p.|)),((f . r0) + (s / |.p.|)).[ as Subset of R^1 by TOPMETR:24;
A10: f . r0 < (f . r0) + (s / |.p.|) by A6, A8, XREAL_1:31, XREAL_1:141;
then (f . r0) - (s / |.p.|) < f . r0 by XREAL_1:21;
then A11: f . r0 in G1 by A10, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W2 being Subset of X such that
A12: ( r0 in W2 & W2 is open & f .: W2 c= G1 ) by A1, A11, JGRAPH_2:20;
g .: W2 c= V

proof

let y be set ; :: 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 set such that
A13: ( r in dom g & r in W2 & y = g . r ) by FUNCT_1:def 12;
reconsider r = r as Point of X by A13;
dom f = the carrier of X by FUNCT_2:def 1;
then f . r in f .: W2 by A13, FUNCT_1:def 12;
then A14: abs ((f . r) - (f . r0)) < s / |.p.| by A12, RCOMP_1:8;
reconsider t = f . r, t0 = f . r0 as Real by XREAL_0:def 1;
A15: abs (t0 - t) = abs (t - t0) by UNIFORM1:13;
reconsider v = g . r as Point of (Euclid n) by TOPREAL3:13;
g . r0 = (f . r0) * p by A3;
then A16: |.((g . r0) - (g . r)).| = |.(((f . r0) * p) - ((f . r) * p)).| by A3
.= |.(((f . r0) - (f . r)) * p).| by EUCLID:54
.= (abs (t0 - t)) * |.p.| by TOPRNS_1:8 ;
(abs ((f . r) - (f . r0))) * |.p.| < (s / |.p.|) * |.p.| by A8, A14, XREAL_1:70;
then |.((g . r0) - (g . r)).| < s by A7, A15, A16, TOPRNS_1:25, XCMPLX_1:88;
then dist u,v < s by JGRAPH_1:45;
then g . r in Ball u,s by METRIC_1:12;
hence y in V by A6, A13; :: thesis: verum

end;

hence ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) by A12; :: thesis: verum

end;

case A17: p = 0. (TOP-REAL n) ; :: thesis: ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )

A18: for r being Point of X holds g . r = 0. (TOP-REAL n)

proof

let r be Point of X; :: thesis: g . r = 0. (TOP-REAL n)
thus g . r = (f . r) * p by A3
.= 0. (TOP-REAL n) by A17, EUCLID:32 ; :: thesis: verum

end;

then A19: 0. (TOP-REAL n) in V by A4;
set W2 = [#] X;
g .: ([#] X) c= V

proof

let y be set ; :: 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 consider x being set such that
A21: ( x in dom g & x in [#] X & y = g . x ) by FUNCT_1:def 12;
thus y in V by A18, A19, A21; :: 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:20;
hence ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous ) by A3; :: thesis: verum