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_{1}[ set , set ] means $2 = (f . $1) * p;

A2: for x being Element of X ex y being Element of (TOP-REAL n) st S_{1}[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_{1}[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_{1}[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 )

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

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

A2: for x being Element of X ex y being Element of (TOP-REAL n) st S

ex g being Function of the carrier of X, the carrier of (TOP-REAL n) st

for x being Element of X holds S

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

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

then
g is continuous
by JGRAPH_2:10;
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;

( r0 in W & W is open & g .: W c= V ) ; :: thesis: verum

end;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 ) ) )end;

hence
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) )
;

end;

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 )

( 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

( r0 in W & W is open & g .: W c= V ) by A13, A14; :: thesis: verum

end;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

hence
ex W being Subset of X st
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;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

( r0 in W & W is open & g .: W c= V ) by A13, A14; :: thesis: verum

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 )

( r0 in W & W is open & g .: W c= V )

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

set W2 = [#] X;

g .: ([#] X) c= V

( r0 in W & W is open & g .: W c= V ) ; :: thesis: verum

end;proof

then A24:
0. (TOP-REAL n) in V
by A4;
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;thus g . r = (f . r) * p by A3

.= 0. (TOP-REAL n) by A22, RLVECT_1:10 ; :: thesis: verum

set W2 = [#] X;

g .: ([#] X) c= V

proof

hence
ex W being Subset of X st
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;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

( r0 in W & W is open & g .: W c= V ) ; :: thesis: verum

( r0 in W & W is open & g .: W c= V ) ; :: thesis: verum

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