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 S1[ 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 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 ;
[#] 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: 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
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
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;
per cases ( fp = 0 or fp <> 0 ) ;
suppose A6: 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 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
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;
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;
for x being ExtReal st x in WW2 holds
x <= |.pp.| + (r0 / 2)
proof
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;
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 ;
A13: m >= 0
per cases ( m = 0 or m > 0 ) by A13;
suppose A16: 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: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
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;
hence g .: W3 c= V by A5; :: thesis: verum
end;
suppose A27: 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: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
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;
hence g .: W3 c= V by A5; :: thesis: verum
end;
end;
end;
suppose A44: 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) / |.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
proof
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;
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;
for x being ExtReal st x in WW2 holds
x <= |.pp.| + ((r0 / 2) / |.fp.|)
proof
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;
then |.pp.| + ((r0 / 2) / |.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 ;
A51: m >= 0
per cases ( m = 0 or m > 0 ) by A51;
suppose A54: 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: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
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;
hence g .: W3 c= V by A5; :: thesis: verum
end;
suppose A68: 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: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
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;
hence g .: W3 c= V by A5; :: 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 st a = b & f . a = r holds
g . b = r * b ) & g is continuous ) by A3, JGRAPH_2:10; :: thesis: verum