let n be natural number ; :: 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 number 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 number 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 number 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 number st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
defpred S1[ set , set ] means for b being Point of (TOP-REAL n)
for r being real number 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 S1[x,y]
proof
let x be Element of X; :: thesis: ex y being Point of (TOP-REAL n) st S1[x,y]
reconsider r = f . x as Real by TOPMETR:24;
A3: x in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
then reconsider p = x as Point of (TOP-REAL n) by A3;
set y = r * p;
take r * p ; :: thesis: S1[x,r * p]
thus S1[x,r * p] ; :: thesis: verum
end;
ex g being Function of the carrier of X, the carrier of (TOP-REAL n) st
for x being Element of X holds S1[x,g . x] from FUNCT_2:sch 3(A2);
 then consider g being Function of X,(TOP-REAL n) such that
A4: for x being Element of X
for b being Point of (TOP-REAL n)
for r being real number 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 number 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
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 ) )
A5: n in NAT by ORDINAL1:def 13;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
reconsider gp = g . p as Point of (Euclid n) by TOPREAL3:13;
A6: p in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
then reconsider pp = p as Point of (TOP-REAL n1) by A6;
reconsider fp = f . p as real number ;
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:55;
then consider r0 being real number such that
A7: r0 > 0 and
A8: Ball (gp,r0) c= V by A5, GOBOARD6:8;
per cases ( fp = 0 or fp <> 0 ) ;
suppose A9: fp = 0 ; :: thesis: ex W being Subset of X st
( 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 5;
then W2 in the topology of X by PRE_TOPC:def 9;
then A10: W2 is open by PRE_TOPC:def 5;
p in Ball (pp,(r0 / 2)) by A7, JORDAN:16;
then A11: p in W2 by XBOOLE_0:def 4;
set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;
A12: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A11;
for x being set st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds
x is real
proof
let x be set ; :: 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
A13: ( x = |.p2.| & p2 in W2 ) ;
thus x is real by A13; :: thesis: verum
end;
then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A12, MEMBERED:def 3;
for x being ext-real number st x in WW2 holds
x <= |.pp.| + (r0 / 2)
proof
let x be ext-real number ; :: 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
A14: ( x = |.p2.| & p2 in W2 ) ;
p2 in Ball (pp,(r0 / 2)) by A14, XBOOLE_0:def 4;
then A15: |.(p2 - pp).| < r0 / 2 by TOPREAL9:7;
|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:32;
then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:27;
then |.p2.| - |.pp.| <= r0 / 2 by A15, XXREAL_0:2;
then (|.p2.| - |.pp.|) + |.pp.| <= (r0 / 2) + |.pp.| by XREAL_1:8;
hence x <= |.pp.| + (r0 / 2) by A14; :: thesis: verum
end;
then |.pp.| + (r0 / 2) is UpperBound of WW2 by XXREAL_2:def 1;
then WW2 is bounded_above by XXREAL_2:def 10;
then reconsider m = sup WW2 as real number ;
A16: m >= 0
per cases ( m = 0 or m > 0 ) by A16;
suppose A19: m = 0 ; :: thesis: ex W being Subset of X st
( 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:24;
then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def 5;
fp in G1 by XREAL_0:def 1;
then consider W1 being Subset of X such that
A20: p in W1 and
A21: W1 is open and
f .: W1 c= G1 by A1, JGRAPH_2:20;
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 A20, A11, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A21, A10; :: thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: 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 set such that
A22: q in dom g and
A23: q in W3 and
A24: g . q = x by FUNCT_1:def 12;
reconsider q = q as Point of X by A22;
A25: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
then reconsider qq = q as Point of (TOP-REAL n1) by A25;
reconsider fq = f . q as real number ;
A26: x = fq * qq by A4, A24;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:13;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A26;
A27: gpp = fp * pp by A4;
reconsider r2 = fq - fp as Real by XREAL_0:def 1;
A28: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.|
.= |.((fq - fp) * qq).| by TOPRNS_1:8 ;
qq in W2 by A23, XBOOLE_0:def 4;
then |.qq.| in WW2 ;
then A29: |.qq.| <= m by XXREAL_2:4;
A30: gpp = 0. (TOP-REAL n1) by A27, A9, EUCLID:33;
|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:74;
then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by JGRAPH_5:13, A30;
then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:61;
then |.(gqq - gpp).| < r0 by A4, A24, A9, A29, A28, A7, A19;
then gqq in Ball (gpp,r0) ;
hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum
end;
hence g .: W3 c= V by A8, XBOOLE_1:1; :: thesis: verum
end;
suppose A31: m > 0 ; :: thesis: ex W being Subset of X st
( 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:46, TOPMETR:24, XXREAL_1:225;
A32: 0 + fp < (r0 / m) + fp by A31, A7, XREAL_1:8;
(- (r0 / m)) + fp < 0 + fp by A31, A7, XREAL_1:8;
then fp in G1 by A32, XXREAL_1:4;
then consider W1 being Subset of X such that
A33: p in W1 and
A34: W1 is open and
A35: f .: W1 c= G1 by A1, JGRAPH_2:20;
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 A33, A11, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A34, A10; :: thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: 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 set such that
A36: q in dom g and
A37: q in W3 and
A38: g . q = x by FUNCT_1:def 12;
reconsider q = q as Point of X by A36;
A39: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
then reconsider qq = q as Point of (TOP-REAL n1) by A39;
reconsider fq = f . q as real number ;
A40: x = fq * qq by A4, A38;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:13;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A40;
A41: gpp = fp * pp by A4;
reconsider r2 = fq as Real by XREAL_0:def 1;
A42: (abs fq) * |.qq.| = (abs r2) * |.qq.|
.= |.(fq * qq).| by TOPRNS_1:8 ;
A43: q in dom f by A39, FUNCT_2:def 1;
q in W1 by A37, XBOOLE_0:def 4;
then f . q in f .: W1 by A43, FUNCT_1:def 12;
then abs (fq - fp) < r0 / m by A35, RCOMP_1:8;
then (abs fq) * m < (r0 / m) * m by A9, A31, XREAL_1:70;
then (abs fq) * m < r0 / (m / m) by XCMPLX_1:83;
then A44: (abs fq) * m < r0 / 1 by A31, XCMPLX_1:60;
qq in W2 by A37, XBOOLE_0:def 4;
then |.qq.| in WW2 ;
then |.qq.| <= m by XXREAL_2:4;
then A45: |.qq.| * (abs fq) <= m * (abs fq) by XREAL_1:66;
A46: gpp = 0. (TOP-REAL n1) by A41, A9, EUCLID:33;
A47: |.gqq.| < r0 by A40, A45, A42, A44, XXREAL_0:2;
|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:74;
then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by JGRAPH_5:13, A46;
then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:61;
then |.(gqq - gpp).| < r0 by A47, XXREAL_0:2;
then gqq in Ball (gpp,r0) ;
hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum
end;
hence g .: W3 c= V by A8, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
suppose A48: fp <> 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
reconsider W2 = (Ball (pp,((r0 / 2) / (abs fp)))) /\ ([#] X) as Subset of X ;
Ball (pp,((r0 / 2) / (abs fp))) in the topology of (TOP-REAL n1) by PRE_TOPC:def 5;
then W2 in the topology of X by PRE_TOPC:def 9;
then A49: W2 is open by PRE_TOPC:def 5;
p in Ball (pp,((r0 / 2) / (abs fp))) by JORDAN:16, A48, A7;
then A50: p in W2 by XBOOLE_0:def 4;
set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;
A51: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A50;
for x being set st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds
x is real
proof
let x be set ; :: 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
A52: ( x = |.p2.| & p2 in W2 ) ;
thus x is real by A52; :: thesis: verum
end;
then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A51, MEMBERED:def 3;
for x being ext-real number st x in WW2 holds
x <= |.pp.| + ((r0 / 2) / (abs fp))
proof
let x be ext-real number ; :: thesis: ( x in WW2 implies x <= |.pp.| + ((r0 / 2) / (abs fp)) )
assume x in WW2 ; :: thesis: x <= |.pp.| + ((r0 / 2) / (abs fp))
then consider p2 being Point of (TOP-REAL n1) such that
A53: ( x = |.p2.| & p2 in W2 ) ;
p2 in Ball (pp,((r0 / 2) / (abs fp))) by A53, XBOOLE_0:def 4;
then A54: |.(p2 - pp).| < (r0 / 2) / (abs fp) by TOPREAL9:7;
|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:32;
then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:27;
then |.p2.| - |.pp.| <= (r0 / 2) / (abs fp) by A54, XXREAL_0:2;
then (|.p2.| - |.pp.|) + |.pp.| <= ((r0 / 2) / (abs fp)) + |.pp.| by XREAL_1:8;
hence x <= |.pp.| + ((r0 / 2) / (abs fp)) by A53; :: thesis: verum
end;
then |.pp.| + ((r0 / 2) / (abs fp)) is UpperBound of WW2 by XXREAL_2:def 1;
then WW2 is bounded_above by XXREAL_2:def 10;
then reconsider m = sup WW2 as real number ;
A55: m >= 0
per cases ( m = 0 or m > 0 ) by A55;
suppose A58: m = 0 ; :: thesis: ex W being Subset of X st
( 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:24;
then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def 5;
fp in G1 by XREAL_0:def 1;
then consider W1 being Subset of X such that
A59: p in W1 and
A60: W1 is open and
f .: W1 c= G1 by A1, JGRAPH_2:20;
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 A59, A50, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A60, A49; :: thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: 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 set such that
A61: q in dom g and
A62: q in W3 and
A63: g . q = x by FUNCT_1:def 12;
reconsider q = q as Point of X by A61;
A64: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
then reconsider qq = q as Point of (TOP-REAL n1) by A64;
reconsider fq = f . q as real number ;
A65: x = fq * qq by A4, A63;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:13;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A65;
A66: gpp = fp * pp by A4;
reconsider r2 = fq - fp as Real by XREAL_0:def 1;
reconsider r3 = fp as Real by XREAL_0:def 1;
A67: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.|
.= |.((fq - fp) * qq).| by TOPRNS_1:8 ;
qq in W2 by A62, XBOOLE_0:def 4;
then |.qq.| in WW2 ;
then A68: |.qq.| <= m by XXREAL_2:4;
A69: (abs fp) * |.(qq - pp).| = (abs r3) * |.(qq - pp).|
.= |.(fp * (qq - pp)).| by TOPRNS_1:8 ;
qq in W2 by A62, XBOOLE_0:def 4;
then qq in Ball (pp,((r0 / 2) / (abs fp))) by XBOOLE_0:def 4;
then |.(qq - pp).| < (r0 / 2) / (abs fp) by TOPREAL9:7;
then (abs fp) * |.(qq - pp).| < (abs fp) * ((r0 / 2) / (abs fp)) by A48, XREAL_1:70;
then (abs fp) * |.(qq - pp).| < (r0 / 2) / ((abs fp) / (abs fp)) by XCMPLX_1:82;
then A70: (abs fp) * |.(qq - pp).| < (r0 / 2) / 1 by A48, XCMPLX_1:60;
A71: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A68, A70, A69, A67, A58, XREAL_1:10;
|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:74;
then A72: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A71, XXREAL_0:2;
((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by EUCLID:54
.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by EUCLID:53
.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by EUCLID:49
.= (fq * qq) - (fp * pp) by EUCLID:52 ;
then gqq in Ball (gpp,r0) by A65, A72, A66;
hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum
end;
hence g .: W3 c= V by A8, XBOOLE_1:1; :: thesis: verum
end;
suppose A73: m > 0 ; :: thesis: ex W being Subset of X st
( 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:46, TOPMETR:24, XXREAL_1:225;
A74: 0 + fp < ((r0 / 2) / m) + fp by A73, A7, XREAL_1:8;
(- ((r0 / 2) / m)) + fp < 0 + fp by A73, A7, XREAL_1:8;
then fp in G1 by A74, XXREAL_1:4;
then consider W1 being Subset of X such that
A75: p in W1 and
A76: W1 is open and
A77: f .: W1 c= G1 by A1, JGRAPH_2:20;
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 A75, A50, XBOOLE_0:def 4; :: thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A76, A49; :: thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: 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 set such that
A78: q in dom g and
A79: q in W3 and
A80: g . q = x by FUNCT_1:def 12;
reconsider q = q as Point of X by A78;
A81: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
then reconsider qq = q as Point of (TOP-REAL n1) by A81;
reconsider fq = f . q as real number ;
A82: x = fq * qq by A4, A80;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:13;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A82;
A83: gpp = fp * pp by A4;
reconsider r2 = fq - fp as Real by XREAL_0:def 1;
reconsider r3 = fp as Real by XREAL_0:def 1;
A84: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.|
.= |.((fq - fp) * qq).| by TOPRNS_1:8 ;
A85: q in dom f by A81, FUNCT_2:def 1;
q in W1 by A79, XBOOLE_0:def 4;
then f . q in f .: W1 by A85, FUNCT_1:def 12;
then abs (fq - fp) < (r0 / 2) / m by A77, RCOMP_1:8;
then (abs (fq - fp)) * m < ((r0 / 2) / m) * m by A73, XREAL_1:70;
then (abs (fq - fp)) * m < (r0 / 2) / (m / m) by XCMPLX_1:83;
then A86: (abs (fq - fp)) * m < (r0 / 2) / 1 by A73, XCMPLX_1:60;
qq in W2 by A79, XBOOLE_0:def 4;
then |.qq.| in WW2 ;
then |.qq.| <= m by XXREAL_2:4;
then |.qq.| * (abs (fq - fp)) <= m * (abs (fq - fp)) by XREAL_1:66;
then A87: |.((fq - fp) * qq).| < r0 / 2 by A84, A86, XXREAL_0:2;
A88: (abs fp) * |.(qq - pp).| = (abs r3) * |.(qq - pp).|
.= |.(fp * (qq - pp)).| by TOPRNS_1:8 ;
qq in W2 by A79, XBOOLE_0:def 4;
then qq in Ball (pp,((r0 / 2) / (abs fp))) by XBOOLE_0:def 4;
then |.(qq - pp).| < (r0 / 2) / (abs fp) by TOPREAL9:7;
then (abs fp) * |.(qq - pp).| < (abs fp) * ((r0 / 2) / (abs fp)) by A48, XREAL_1:70;
then (abs fp) * |.(qq - pp).| < (r0 / 2) / ((abs fp) / (abs fp)) by XCMPLX_1:82;
then A89: (abs fp) * |.(qq - pp).| < (r0 / 2) / 1 by A48, XCMPLX_1:60;
A90: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A87, A89, A88, XREAL_1:10;
|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:74;
then A91: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A90, XXREAL_0:2;
((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by EUCLID:54
.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by EUCLID:53
.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by EUCLID:49
.= (fq * qq) - (fp * pp) by EUCLID:52 ;
then gqq in Ball (gpp,r0) by A82, A83, A91;
hence x in Ball (gp,r0) by TOPREAL9:13; :: thesis: verum
end;
hence g .: W3 c= V by A8, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
end;
end;
hence ( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous ) by A4, JGRAPH_2:20; :: thesis: verum