let X be non empty TopSpace; :: thesis: for n being 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 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 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 A4, A5, TOPS_1:23;
reconsider u = g . r0 as Point of (Euclid n) by TOPREAL3:8;
consider s being Real such that
A7: s > 0 and
A8: Ball (u,s) c= V by A6, GOBOARD6:5;

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

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

case A9: p <> 0. (TOP-REAL n) ; :: 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 A7, A10, XREAL_1:29, XREAL_1:139;
then (f . r0) - (s / |.p.|) < f . r0 by XREAL_1:19;
then A12: f . r0 in G1 by A11, XXREAL_1:4;
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 A1, A12, JGRAPH_2:10;
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 A17, FUNCT_1:def 6;
then A19: |.((f . r) - (f . r0)).| < s / |.p.| by A15, RCOMP_1:1;
reconsider t = f . r, t0 = f . r0 as Real ;
A20: |.(t0 - t).| = |.(t - t0).| by UNIFORM1:11;
reconsider v = g . r as Point of (Euclid n) 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 A10, A19, XREAL_1:68;
then |.((g . r0) - (g . r)).| < s by A9, A20, A21, TOPRNS_1:24, XCMPLX_1:87;
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 A8, A18; :: thesis: verum

end;

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

end;

case A22: p = 0. (TOP-REAL n) ; :: 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. (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 A22, RLVECT_1:10 ; :: thesis: verum

end;

then A24: 0. (TOP-REAL n) 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 A23, A24; :: 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,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous ) by A3; :: thesis: verum