let n be Nat; :: thesis: for X being non empty SubSpace 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 a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous )

let X be non empty SubSpace 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 a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & 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 a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous ) )

assume A1: f is continuous ; :: thesis: ex g being Function of X,(TOP-REAL n) st

( ( for a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous )

defpred S_{1}[ set , set ] means for b being Point of (TOP-REAL n)

for r being Real st $1 = b & f . $1 = r holds

$2 = r * b;

A2: for x being Element of X ex y being Point of (TOP-REAL n) st S_{1}[x,y]

for x being Element of X holds S_{1}[x,g . x]
from FUNCT_2:sch 3(A2);

then consider g being Function of X,(TOP-REAL n) such that

A3: for x being Element of X

for b being Point of (TOP-REAL n)

for r being Real st x = b & f . x = r holds

g . x = r * b ;

take g ; :: thesis: ( ( for a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous )

for p being Point of X

for V being Subset of (TOP-REAL n) st g . p in V & V is open holds

ex W being Subset of X st

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

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous ) by A3, JGRAPH_2:10; :: thesis: verum

for f being Function of X,R^1 st f is continuous holds

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

( ( for a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous )

let X be non empty SubSpace 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 a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & 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 a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous ) )

assume A1: f is continuous ; :: thesis: ex g being Function of X,(TOP-REAL n) st

( ( for a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous )

defpred S

for r being Real st $1 = b & f . $1 = r holds

$2 = r * b;

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

proof

ex g being Function of the carrier of X, the carrier of (TOP-REAL n) st
let x be Element of X; :: thesis: ex y being Point of (TOP-REAL n) st S_{1}[x,y]

reconsider r = f . x as Real ;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider p = x as Point of (TOP-REAL n) ;

set y = r * p;

take r * p ; :: thesis: S_{1}[x,r * p]

thus S_{1}[x,r * p]
; :: thesis: verum

end;reconsider r = f . x as Real ;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider p = x as Point of (TOP-REAL n) ;

set y = r * p;

take r * p ; :: thesis: S

thus S

for x being Element of X holds S

then consider g being Function of X,(TOP-REAL n) such that

A3: for x being Element of X

for b being Point of (TOP-REAL n)

for r being Real st x = b & f . x = r holds

g . x = r * b ;

take g ; :: thesis: ( ( for a being Point of X

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous )

for p being Point of X

for V being Subset of (TOP-REAL n) st g . p in V & V is open holds

ex W being Subset of X st

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

proof

hence
( ( for a being Point of X
let p be Point of X; :: thesis: for V being Subset of (TOP-REAL n) st g . p in V & V is open holds

ex W being Subset of X st

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

let V be Subset of (TOP-REAL n); :: thesis: ( g . p in V & V is open implies ex W being Subset of X st

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

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider gp = g . p as Point of (Euclid n) by TOPREAL3:8;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider pp = p as Point of (TOP-REAL n1) ;

reconsider fp = f . p as Real ;

assume ( g . p in V & V is open ) ; :: thesis: ex W being Subset of X st

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

then g . p in Int V by TOPS_1:23;

then consider r0 being Real such that

A4: r0 > 0 and

A5: Ball (gp,r0) c= V by GOBOARD6:5;

end;ex W being Subset of X st

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

let V be Subset of (TOP-REAL n); :: thesis: ( g . p in V & V is open implies ex W being Subset of X st

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

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider gp = g . p as Point of (Euclid n) by TOPREAL3:8;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider pp = p as Point of (TOP-REAL n1) ;

reconsider fp = f . p as Real ;

assume ( g . p in V & V is open ) ; :: thesis: ex W being Subset of X st

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

then g . p in Int V by TOPS_1:23;

then consider r0 being Real such that

A4: r0 > 0 and

A5: Ball (gp,r0) c= V by GOBOARD6:5;

per cases
( fp = 0 or fp <> 0 )
;

end;

suppose A6:
fp = 0
; :: thesis: ex W being Subset of X st

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

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

reconsider W2 = (Ball (pp,(r0 / 2))) /\ ([#] X) as Subset of X ;

Ball (pp,(r0 / 2)) in the topology of (TOP-REAL n1) by PRE_TOPC:def 2;

then W2 in the topology of X by PRE_TOPC:def 4;

then A7: W2 is open by PRE_TOPC:def 2;

p in Ball (pp,(r0 / 2)) by A4, JORDAN:16;

then A8: p in W2 by XBOOLE_0:def 4;

set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;

A9: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A8;

for x being object st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds

x is real

for x being ExtReal st x in WW2 holds

x <= |.pp.| + (r0 / 2)

then WW2 is bounded_above by XXREAL_2:def 10;

then reconsider m = sup WW2 as Real ;

A13: m >= 0

end;Ball (pp,(r0 / 2)) in the topology of (TOP-REAL n1) by PRE_TOPC:def 2;

then W2 in the topology of X by PRE_TOPC:def 4;

then A7: W2 is open by PRE_TOPC:def 2;

p in Ball (pp,(r0 / 2)) by A4, JORDAN:16;

then A8: p in W2 by XBOOLE_0:def 4;

set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;

A9: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A8;

for x being object st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds

x is real

proof

then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A9, MEMBERED:def 3;
let x be object ; :: thesis: ( x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } implies x is real )

assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; :: thesis: x is real

then consider p2 being Point of (TOP-REAL n1) such that

A10: ( x = |.p2.| & p2 in W2 ) ;

thus x is real by A10; :: thesis: verum

end;assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; :: thesis: x is real

then consider p2 being Point of (TOP-REAL n1) such that

A10: ( x = |.p2.| & p2 in W2 ) ;

thus x is real by A10; :: thesis: verum

for x being ExtReal st x in WW2 holds

x <= |.pp.| + (r0 / 2)

proof

then
|.pp.| + (r0 / 2) is UpperBound of WW2
by XXREAL_2:def 1;
let x be ExtReal; :: thesis: ( x in WW2 implies x <= |.pp.| + (r0 / 2) )

assume x in WW2 ; :: thesis: x <= |.pp.| + (r0 / 2)

then consider p2 being Point of (TOP-REAL n1) such that

A11: ( x = |.p2.| & p2 in W2 ) ;

p2 in Ball (pp,(r0 / 2)) by A11, XBOOLE_0:def 4;

then A12: |.(p2 - pp).| < r0 / 2 by TOPREAL9:7;

|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:31;

then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:26;

then |.p2.| - |.pp.| <= r0 / 2 by A12, XXREAL_0:2;

then (|.p2.| - |.pp.|) + |.pp.| <= (r0 / 2) + |.pp.| by XREAL_1:6;

hence x <= |.pp.| + (r0 / 2) by A11; :: thesis: verum

end;assume x in WW2 ; :: thesis: x <= |.pp.| + (r0 / 2)

then consider p2 being Point of (TOP-REAL n1) such that

A11: ( x = |.p2.| & p2 in W2 ) ;

p2 in Ball (pp,(r0 / 2)) by A11, XBOOLE_0:def 4;

then A12: |.(p2 - pp).| < r0 / 2 by TOPREAL9:7;

|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:31;

then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:26;

then |.p2.| - |.pp.| <= r0 / 2 by A12, XXREAL_0:2;

then (|.p2.| - |.pp.|) + |.pp.| <= (r0 / 2) + |.pp.| by XREAL_1:6;

hence x <= |.pp.| + (r0 / 2) by A11; :: thesis: verum

then WW2 is bounded_above by XXREAL_2:def 10;

then reconsider m = sup WW2 as Real ;

A13: m >= 0

proof

assume A14:
m < 0
; :: thesis: contradiction

A15: m is UpperBound of WW2 by XXREAL_2:def 3;

|.pp.| in WW2 by A8;

hence contradiction by A14, A15, XXREAL_2:def 1; :: thesis: verum

end;A15: m is UpperBound of WW2 by XXREAL_2:def 3;

|.pp.| in WW2 by A8;

hence contradiction by A14, A15, XXREAL_2:def 1; :: thesis: verum

per cases
( m = 0 or m > 0 )
by A13;

end;

suppose A16:
m = 0
; :: thesis: ex W being Subset of X st

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

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

set G1 = REAL ;

REAL in the topology of R^1 by PRE_TOPC:def 1, TOPMETR:17;

then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def 2;

fp in G1 by XREAL_0:def 1;

then consider W1 being Subset of X such that

A17: p in W1 and

A18: W1 is open and

f .: W1 c= G1 by A1, JGRAPH_2:10;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A17, A8, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A18, A7; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

end;REAL in the topology of R^1 by PRE_TOPC:def 1, TOPMETR:17;

then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def 2;

fp in G1 by XREAL_0:def 1;

then consider W1 being Subset of X such that

A17: p in W1 and

A18: W1 is open and

f .: W1 c= G1 by A1, JGRAPH_2:10;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A17, A8, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A18, A7; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

proof

hence
g .: W3 c= V
by A5; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: W3 or x in Ball (gp,r0) )

assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A19: q in dom g and

A20: q in W3 and

A21: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A19;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A22: x = fq * qq by A3, A21;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A22;

A23: gpp = fp * pp by A3;

reconsider r2 = fq - fp as Real ;

A24: |.(fq - fp).| * |.qq.| = |.r2.| * |.qq.|

.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;

qq in W2 by A20, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then A25: |.qq.| <= m by XXREAL_2:4;

A26: gpp = 0. (TOP-REAL n1) by A23, A6, RLVECT_1:10;

|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52;

then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A26, JGRAPH_5:10;

then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39;

then |.(gqq - gpp).| < r0 by A3, A21, A6, A25, A24, A4, A16;

then gqq in Ball (gpp,r0) ;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

end;assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A19: q in dom g and

A20: q in W3 and

A21: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A19;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A22: x = fq * qq by A3, A21;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A22;

A23: gpp = fp * pp by A3;

reconsider r2 = fq - fp as Real ;

A24: |.(fq - fp).| * |.qq.| = |.r2.| * |.qq.|

.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;

qq in W2 by A20, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then A25: |.qq.| <= m by XXREAL_2:4;

A26: gpp = 0. (TOP-REAL n1) by A23, A6, RLVECT_1:10;

|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52;

then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A26, JGRAPH_5:10;

then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39;

then |.(gqq - gpp).| < r0 by A3, A21, A6, A25, A24, A4, A16;

then gqq in Ball (gpp,r0) ;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

suppose A27:
m > 0
; :: thesis: ex W being Subset of X st

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

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

set G1 = ].(fp - (r0 / m)),(fp + (r0 / m)).[;

reconsider G1 = ].(fp - (r0 / m)),(fp + (r0 / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;

A28: 0 + fp < (r0 / m) + fp by A27, A4, XREAL_1:6;

(- (r0 / m)) + fp < 0 + fp by A27, A4, XREAL_1:6;

then consider W1 being Subset of X such that

A29: p in W1 and

A30: W1 is open and

A31: f .: W1 c= G1 by A1, JGRAPH_2:10, A28, XXREAL_1:4;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A29, A8, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A30, A7; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

end;reconsider G1 = ].(fp - (r0 / m)),(fp + (r0 / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;

A28: 0 + fp < (r0 / m) + fp by A27, A4, XREAL_1:6;

(- (r0 / m)) + fp < 0 + fp by A27, A4, XREAL_1:6;

then consider W1 being Subset of X such that

A29: p in W1 and

A30: W1 is open and

A31: f .: W1 c= G1 by A1, JGRAPH_2:10, A28, XXREAL_1:4;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A29, A8, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A30, A7; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

proof

hence
g .: W3 c= V
by A5; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: W3 or x in Ball (gp,r0) )

assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A32: q in dom g and

A33: q in W3 and

A34: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A32;

A35: q in the carrier of X ;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A36: x = fq * qq by A3, A34;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A36;

A37: gpp = fp * pp by A3;

reconsider r2 = fq as Real ;

A38: |.fq.| * |.qq.| = |.r2.| * |.qq.|

.= |.(fq * qq).| by TOPRNS_1:7 ;

A39: q in dom f by A35, FUNCT_2:def 1;

q in W1 by A33, XBOOLE_0:def 4;

then f . q in f .: W1 by A39, FUNCT_1:def 6;

then |.(fq - fp).| < r0 / m by A31, RCOMP_1:1;

then |.fq.| * m < (r0 / m) * m by A6, A27, XREAL_1:68;

then |.fq.| * m < r0 / (m / m) by XCMPLX_1:82;

then A40: |.fq.| * m < r0 / 1 by A27, XCMPLX_1:60;

qq in W2 by A33, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then |.qq.| <= m by XXREAL_2:4;

then A41: |.qq.| * |.fq.| <= m * |.fq.| by XREAL_1:64;

A42: gpp = 0. (TOP-REAL n1) by A37, A6, RLVECT_1:10;

A43: |.gqq.| < r0 by A36, A41, A38, A40, XXREAL_0:2;

|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52;

then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A42, JGRAPH_5:10;

then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39;

then |.(gqq - gpp).| < r0 by A43, XXREAL_0:2;

then gqq in Ball (gpp,r0) ;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

end;assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A32: q in dom g and

A33: q in W3 and

A34: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A32;

A35: q in the carrier of X ;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A36: x = fq * qq by A3, A34;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A36;

A37: gpp = fp * pp by A3;

reconsider r2 = fq as Real ;

A38: |.fq.| * |.qq.| = |.r2.| * |.qq.|

.= |.(fq * qq).| by TOPRNS_1:7 ;

A39: q in dom f by A35, FUNCT_2:def 1;

q in W1 by A33, XBOOLE_0:def 4;

then f . q in f .: W1 by A39, FUNCT_1:def 6;

then |.(fq - fp).| < r0 / m by A31, RCOMP_1:1;

then |.fq.| * m < (r0 / m) * m by A6, A27, XREAL_1:68;

then |.fq.| * m < r0 / (m / m) by XCMPLX_1:82;

then A40: |.fq.| * m < r0 / 1 by A27, XCMPLX_1:60;

qq in W2 by A33, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then |.qq.| <= m by XXREAL_2:4;

then A41: |.qq.| * |.fq.| <= m * |.fq.| by XREAL_1:64;

A42: gpp = 0. (TOP-REAL n1) by A37, A6, RLVECT_1:10;

A43: |.gqq.| < r0 by A36, A41, A38, A40, XXREAL_0:2;

|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52;

then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A42, JGRAPH_5:10;

then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39;

then |.(gqq - gpp).| < r0 by A43, XXREAL_0:2;

then gqq in Ball (gpp,r0) ;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

suppose A44:
fp <> 0
; :: thesis: ex W being Subset of X st

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

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

reconsider W2 = (Ball (pp,((r0 / 2) / |.fp.|))) /\ ([#] X) as Subset of X ;

Ball (pp,((r0 / 2) / |.fp.|)) in the topology of (TOP-REAL n1) by PRE_TOPC:def 2;

then W2 in the topology of X by PRE_TOPC:def 4;

then A45: W2 is open by PRE_TOPC:def 2;

p in Ball (pp,((r0 / 2) / |.fp.|)) by A44, A4, JORDAN:16;

then A46: p in W2 by XBOOLE_0:def 4;

set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;

A47: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A46;

for x being object st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds

x is real

for x being ExtReal st x in WW2 holds

x <= |.pp.| + ((r0 / 2) / |.fp.|)

then WW2 is bounded_above by XXREAL_2:def 10;

then reconsider m = sup WW2 as Real ;

A51: m >= 0

end;Ball (pp,((r0 / 2) / |.fp.|)) in the topology of (TOP-REAL n1) by PRE_TOPC:def 2;

then W2 in the topology of X by PRE_TOPC:def 4;

then A45: W2 is open by PRE_TOPC:def 2;

p in Ball (pp,((r0 / 2) / |.fp.|)) by A44, A4, JORDAN:16;

then A46: p in W2 by XBOOLE_0:def 4;

set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;

A47: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A46;

for x being object st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds

x is real

proof

then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A47, MEMBERED:def 3;
let x be object ; :: thesis: ( x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } implies x is real )

assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; :: thesis: x is real

then consider p2 being Point of (TOP-REAL n1) such that

A48: ( x = |.p2.| & p2 in W2 ) ;

thus x is real by A48; :: thesis: verum

end;assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; :: thesis: x is real

then consider p2 being Point of (TOP-REAL n1) such that

A48: ( x = |.p2.| & p2 in W2 ) ;

thus x is real by A48; :: thesis: verum

for x being ExtReal st x in WW2 holds

x <= |.pp.| + ((r0 / 2) / |.fp.|)

proof

then
|.pp.| + ((r0 / 2) / |.fp.|) is UpperBound of WW2
by XXREAL_2:def 1;
let x be ExtReal; :: thesis: ( x in WW2 implies x <= |.pp.| + ((r0 / 2) / |.fp.|) )

assume x in WW2 ; :: thesis: x <= |.pp.| + ((r0 / 2) / |.fp.|)

then consider p2 being Point of (TOP-REAL n1) such that

A49: ( x = |.p2.| & p2 in W2 ) ;

p2 in Ball (pp,((r0 / 2) / |.fp.|)) by A49, XBOOLE_0:def 4;

then A50: |.(p2 - pp).| < (r0 / 2) / |.fp.| by TOPREAL9:7;

|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:31;

then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:26;

then |.p2.| - |.pp.| <= (r0 / 2) / |.fp.| by A50, XXREAL_0:2;

then (|.p2.| - |.pp.|) + |.pp.| <= ((r0 / 2) / |.fp.|) + |.pp.| by XREAL_1:6;

hence x <= |.pp.| + ((r0 / 2) / |.fp.|) by A49; :: thesis: verum

end;assume x in WW2 ; :: thesis: x <= |.pp.| + ((r0 / 2) / |.fp.|)

then consider p2 being Point of (TOP-REAL n1) such that

A49: ( x = |.p2.| & p2 in W2 ) ;

p2 in Ball (pp,((r0 / 2) / |.fp.|)) by A49, XBOOLE_0:def 4;

then A50: |.(p2 - pp).| < (r0 / 2) / |.fp.| by TOPREAL9:7;

|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:31;

then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:26;

then |.p2.| - |.pp.| <= (r0 / 2) / |.fp.| by A50, XXREAL_0:2;

then (|.p2.| - |.pp.|) + |.pp.| <= ((r0 / 2) / |.fp.|) + |.pp.| by XREAL_1:6;

hence x <= |.pp.| + ((r0 / 2) / |.fp.|) by A49; :: thesis: verum

then WW2 is bounded_above by XXREAL_2:def 10;

then reconsider m = sup WW2 as Real ;

A51: m >= 0

proof

assume A52:
m < 0
; :: thesis: contradiction

A53: m is UpperBound of WW2 by XXREAL_2:def 3;

|.pp.| in WW2 by A46;

hence contradiction by A52, A53, XXREAL_2:def 1; :: thesis: verum

end;A53: m is UpperBound of WW2 by XXREAL_2:def 3;

|.pp.| in WW2 by A46;

hence contradiction by A52, A53, XXREAL_2:def 1; :: thesis: verum

per cases
( m = 0 or m > 0 )
by A51;

end;

suppose A54:
m = 0
; :: thesis: ex W being Subset of X st

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

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

set G1 = REAL ;

REAL in the topology of R^1 by PRE_TOPC:def 1, TOPMETR:17;

then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def 2;

fp in G1 by XREAL_0:def 1;

then consider W1 being Subset of X such that

A55: p in W1 and

A56: W1 is open and

f .: W1 c= G1 by A1, JGRAPH_2:10;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A55, A46, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A56, A45; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

end;REAL in the topology of R^1 by PRE_TOPC:def 1, TOPMETR:17;

then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def 2;

fp in G1 by XREAL_0:def 1;

then consider W1 being Subset of X such that

A55: p in W1 and

A56: W1 is open and

f .: W1 c= G1 by A1, JGRAPH_2:10;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A55, A46, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A56, A45; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

proof

hence
g .: W3 c= V
by A5; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: W3 or x in Ball (gp,r0) )

assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A57: q in dom g and

A58: q in W3 and

A59: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A57;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A60: x = fq * qq by A3, A59;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A60;

A61: gpp = fp * pp by A3;

reconsider r2 = fq - fp as Real ;

reconsider r3 = fp as Real ;

A62: |.(fq - fp).| * |.qq.| = |.r2.| * |.qq.|

.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;

qq in W2 by A58, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then A63: |.qq.| <= m by XXREAL_2:4;

A64: |.fp.| * |.(qq - pp).| = |.r3.| * |.(qq - pp).|

.= |.(fp * (qq - pp)).| by TOPRNS_1:7 ;

qq in W2 by A58, XBOOLE_0:def 4;

then qq in Ball (pp,((r0 / 2) / |.fp.|)) by XBOOLE_0:def 4;

then |.fp.| * |.(qq - pp).| < |.fp.| * ((r0 / 2) / |.fp.|) by A44, XREAL_1:68, TOPREAL9:7;

then |.fp.| * |.(qq - pp).| < (r0 / 2) / (|.fp.| / |.fp.|) by XCMPLX_1:81;

then A65: |.fp.| * |.(qq - pp).| < (r0 / 2) / 1 by A44, XCMPLX_1:60;

A66: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A63, A65, A64, A62, A54, XREAL_1:8;

|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52;

then A67: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A66, XXREAL_0:2;

((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by RLVECT_1:35

.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by RLVECT_1:34

.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by RLVECT_1:def 3

.= (fq * qq) - (fp * pp) by RLVECT_4:1 ;

then gqq in Ball (gpp,r0) by A60, A67, A61;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

end;assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A57: q in dom g and

A58: q in W3 and

A59: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A57;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A60: x = fq * qq by A3, A59;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A60;

A61: gpp = fp * pp by A3;

reconsider r2 = fq - fp as Real ;

reconsider r3 = fp as Real ;

A62: |.(fq - fp).| * |.qq.| = |.r2.| * |.qq.|

.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;

qq in W2 by A58, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then A63: |.qq.| <= m by XXREAL_2:4;

A64: |.fp.| * |.(qq - pp).| = |.r3.| * |.(qq - pp).|

.= |.(fp * (qq - pp)).| by TOPRNS_1:7 ;

qq in W2 by A58, XBOOLE_0:def 4;

then qq in Ball (pp,((r0 / 2) / |.fp.|)) by XBOOLE_0:def 4;

then |.fp.| * |.(qq - pp).| < |.fp.| * ((r0 / 2) / |.fp.|) by A44, XREAL_1:68, TOPREAL9:7;

then |.fp.| * |.(qq - pp).| < (r0 / 2) / (|.fp.| / |.fp.|) by XCMPLX_1:81;

then A65: |.fp.| * |.(qq - pp).| < (r0 / 2) / 1 by A44, XCMPLX_1:60;

A66: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A63, A65, A64, A62, A54, XREAL_1:8;

|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52;

then A67: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A66, XXREAL_0:2;

((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by RLVECT_1:35

.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by RLVECT_1:34

.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by RLVECT_1:def 3

.= (fq * qq) - (fp * pp) by RLVECT_4:1 ;

then gqq in Ball (gpp,r0) by A60, A67, A61;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

suppose A68:
m > 0
; :: thesis: ex W being Subset of X st

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

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

set G1 = ].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[;

reconsider G1 = ].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;

A69: 0 + fp < ((r0 / 2) / m) + fp by A68, A4, XREAL_1:6;

(- ((r0 / 2) / m)) + fp < 0 + fp by A68, A4, XREAL_1:6;

then consider W1 being Subset of X such that

A70: p in W1 and

A71: W1 is open and

A72: f .: W1 c= G1 by A1, JGRAPH_2:10, A69, XXREAL_1:4;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A70, A46, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A71, A45; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

end;reconsider G1 = ].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;

A69: 0 + fp < ((r0 / 2) / m) + fp by A68, A4, XREAL_1:6;

(- ((r0 / 2) / m)) + fp < 0 + fp by A68, A4, XREAL_1:6;

then consider W1 being Subset of X such that

A70: p in W1 and

A71: W1 is open and

A72: f .: W1 c= G1 by A1, JGRAPH_2:10, A69, XXREAL_1:4;

reconsider W3 = W1 /\ W2 as Subset of X ;

take W3 ; :: thesis: ( p in W3 & W3 is open & g .: W3 c= V )

thus p in W3 by A70, A46, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )

thus W3 is open by A71, A45; :: thesis: g .: W3 c= V

g .: W3 c= Ball (gp,r0)

proof

hence
g .: W3 c= V
by A5; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: W3 or x in Ball (gp,r0) )

assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A73: q in dom g and

A74: q in W3 and

A75: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A73;

A76: q in the carrier of X ;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A77: x = fq * qq by A3, A75;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A77;

A78: gpp = fp * pp by A3;

reconsider r2 = fq - fp as Real ;

reconsider r3 = fp as Real ;

A79: |.(fq - fp).| * |.qq.| = |.r2.| * |.qq.|

.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;

A80: q in dom f by A76, FUNCT_2:def 1;

q in W1 by A74, XBOOLE_0:def 4;

then f . q in f .: W1 by A80, FUNCT_1:def 6;

then |.(fq - fp).| * m < ((r0 / 2) / m) * m by A68, XREAL_1:68, A72, RCOMP_1:1;

then |.(fq - fp).| * m < (r0 / 2) / (m / m) by XCMPLX_1:82;

then A81: |.(fq - fp).| * m < (r0 / 2) / 1 by A68, XCMPLX_1:60;

qq in W2 by A74, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then |.qq.| <= m by XXREAL_2:4;

then |.qq.| * |.(fq - fp).| <= m * |.(fq - fp).| by XREAL_1:64;

then A82: |.((fq - fp) * qq).| < r0 / 2 by A79, A81, XXREAL_0:2;

A83: |.fp.| * |.(qq - pp).| = |.r3.| * |.(qq - pp).|

.= |.(fp * (qq - pp)).| by TOPRNS_1:7 ;

qq in W2 by A74, XBOOLE_0:def 4;

then qq in Ball (pp,((r0 / 2) / |.fp.|)) by XBOOLE_0:def 4;

then |.fp.| * |.(qq - pp).| < |.fp.| * ((r0 / 2) / |.fp.|) by A44, XREAL_1:68, TOPREAL9:7;

then |.fp.| * |.(qq - pp).| < (r0 / 2) / (|.fp.| / |.fp.|) by XCMPLX_1:81;

then A84: |.fp.| * |.(qq - pp).| < (r0 / 2) / 1 by A44, XCMPLX_1:60;

A85: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A82, A84, A83, XREAL_1:8;

|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52;

then A86: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A85, XXREAL_0:2;

((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by RLVECT_1:35

.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by RLVECT_1:34

.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by RLVECT_1:def 3

.= (fq * qq) - (fp * pp) by RLVECT_4:1 ;

then gqq in Ball (gpp,r0) by A77, A78, A86;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

end;assume x in g .: W3 ; :: thesis: x in Ball (gp,r0)

then consider q being object such that

A73: q in dom g and

A74: q in W3 and

A75: g . q = x by FUNCT_1:def 6;

reconsider q = q as Point of X by A73;

A76: q in the carrier of X ;

[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qq = q as Point of (TOP-REAL n1) ;

reconsider fq = f . q as Real ;

A77: x = fq * qq by A3, A75;

then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;

reconsider gpp = gp as Point of (TOP-REAL n1) ;

reconsider gqq = gq as Point of (TOP-REAL n1) by A77;

A78: gpp = fp * pp by A3;

reconsider r2 = fq - fp as Real ;

reconsider r3 = fp as Real ;

A79: |.(fq - fp).| * |.qq.| = |.r2.| * |.qq.|

.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;

A80: q in dom f by A76, FUNCT_2:def 1;

q in W1 by A74, XBOOLE_0:def 4;

then f . q in f .: W1 by A80, FUNCT_1:def 6;

then |.(fq - fp).| * m < ((r0 / 2) / m) * m by A68, XREAL_1:68, A72, RCOMP_1:1;

then |.(fq - fp).| * m < (r0 / 2) / (m / m) by XCMPLX_1:82;

then A81: |.(fq - fp).| * m < (r0 / 2) / 1 by A68, XCMPLX_1:60;

qq in W2 by A74, XBOOLE_0:def 4;

then |.qq.| in WW2 ;

then |.qq.| <= m by XXREAL_2:4;

then |.qq.| * |.(fq - fp).| <= m * |.(fq - fp).| by XREAL_1:64;

then A82: |.((fq - fp) * qq).| < r0 / 2 by A79, A81, XXREAL_0:2;

A83: |.fp.| * |.(qq - pp).| = |.r3.| * |.(qq - pp).|

.= |.(fp * (qq - pp)).| by TOPRNS_1:7 ;

qq in W2 by A74, XBOOLE_0:def 4;

then qq in Ball (pp,((r0 / 2) / |.fp.|)) by XBOOLE_0:def 4;

then |.fp.| * |.(qq - pp).| < |.fp.| * ((r0 / 2) / |.fp.|) by A44, XREAL_1:68, TOPREAL9:7;

then |.fp.| * |.(qq - pp).| < (r0 / 2) / (|.fp.| / |.fp.|) by XCMPLX_1:81;

then A84: |.fp.| * |.(qq - pp).| < (r0 / 2) / 1 by A44, XCMPLX_1:60;

A85: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A82, A84, A83, XREAL_1:8;

|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52;

then A86: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A85, XXREAL_0:2;

((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by RLVECT_1:35

.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by RLVECT_1:34

.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by RLVECT_1:def 3

.= (fq * qq) - (fp * pp) by RLVECT_4:1 ;

then gqq in Ball (gpp,r0) by A77, A78, A86;

hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum

for b being Point of (TOP-REAL n)

for r being Real st a = b & f . a = r holds

g . b = r * b ) & g is continuous ) by A3, JGRAPH_2:10; :: thesis: verum