let X be non empty TopSpace; :: thesis: for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X ex r being Real st

( f1 . q = r & r >= 0 ) ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous )

let f1 be Function of X,R^1; :: thesis: ( f1 is continuous & ( for q being Point of X ex r being Real st

( f1 . q = r & r >= 0 ) ) implies ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous ) )

assume that

A1: f1 is continuous and

A2: for q being Point of X ex r being Real st

( f1 . q = r & r >= 0 ) ; :: thesis: ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous )

defpred S_{1}[ set , set ] means for r11 being Real st f1 . $1 = r11 holds

$2 = sqrt r11;

A3: for x being Element of X ex y being Element of REAL st S_{1}[x,y]

for x2 being Element of X holds S_{1}[x2,f . x2]
from FUNCT_2:sch 3(A3);

then consider f being Function of the carrier of X,REAL such that

A4: for x2 being Element of X

for r11 being Real st f1 . x2 = r11 holds

f . x2 = sqrt r11 ;

reconsider g0 = f as Function of X,R^1 by TOPMETR:17;

for p being Point of X

for V being Subset of R^1 st g0 . p in V & V is open holds

ex W being Subset of X st

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

for p being Point of X

for r11 being Real st f1 . p = r11 holds

g0 . p = sqrt r11 by A4;

hence ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous ) by A47; :: thesis: verum

( f1 . q = r & r >= 0 ) ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous )

let f1 be Function of X,R^1; :: thesis: ( f1 is continuous & ( for q being Point of X ex r being Real st

( f1 . q = r & r >= 0 ) ) implies ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous ) )

assume that

A1: f1 is continuous and

A2: for q being Point of X ex r being Real st

( f1 . q = r & r >= 0 ) ; :: thesis: ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous )

defpred S

$2 = sqrt r11;

A3: for x being Element of X ex y being Element of REAL st S

proof

ex f being Function of the carrier of X,REAL st
let x be Element of X; :: thesis: ex y being Element of REAL st S_{1}[x,y]

reconsider r1 = f1 . x as Element of REAL by TOPMETR:17;

reconsider y = sqrt r1 as Element of REAL by XREAL_0:def 1;

take y ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;reconsider r1 = f1 . x as Element of REAL by TOPMETR:17;

reconsider y = sqrt r1 as Element of REAL by XREAL_0:def 1;

take y ; :: thesis: S

thus S

for x2 being Element of X holds S

then consider f being Function of the carrier of X,REAL such that

A4: for x2 being Element of X

for r11 being Real st f1 . x2 = r11 holds

f . x2 = sqrt r11 ;

reconsider g0 = f as Function of X,R^1 by TOPMETR:17;

for p being Point of X

for V being Subset of R^1 st g0 . p in V & V is open holds

ex W being Subset of X st

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

proof

then A47:
g0 is continuous
by JGRAPH_2:10;
let p be Point of X; :: thesis: for V being Subset of R^1 st g0 . p in V & V is open holds

ex W being Subset of X st

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

let V be Subset of R^1; :: thesis: ( g0 . p in V & V is open implies ex W being Subset of X st

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

reconsider r = g0 . p as Real ;

reconsider r1 = f1 . p as Real ;

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

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

then consider r01 being Real such that

A5: r01 > 0 and

A6: ].(r - r01),(r + r01).[ c= V by FRECHET:8;

set r0 = min (r01,1);

A7: min (r01,1) > 0 by A5, XXREAL_0:21;

A8: min (r01,1) > 0 by A5, XXREAL_0:21;

min (r01,1) <= r01 by XXREAL_0:17;

then ( r - r01 <= r - (min (r01,1)) & r + (min (r01,1)) <= r + r01 ) by XREAL_1:6, XREAL_1:10;

then ].(r - (min (r01,1))),(r + (min (r01,1))).[ c= ].(r - r01),(r + r01).[ by XXREAL_1:46;

then A9: ].(r - (min (r01,1))),(r + (min (r01,1))).[ c= V by A6;

A10: ex r8 being Real st

( f1 . p = r8 & r8 >= 0 ) by A2;

A11: r = sqrt r1 by A4;

then A12: r1 = r ^2 by A10, SQUARE_1:def 2;

A13: r >= 0 by A10, A11, SQUARE_1:17, SQUARE_1:26;

then A14: ((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2) > 0 + 0 by A8, SQUARE_1:12, XREAL_1:8;

end;ex W being Subset of X st

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

let V be Subset of R^1; :: thesis: ( g0 . p in V & V is open implies ex W being Subset of X st

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

reconsider r = g0 . p as Real ;

reconsider r1 = f1 . p as Real ;

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

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

then consider r01 being Real such that

A5: r01 > 0 and

A6: ].(r - r01),(r + r01).[ c= V by FRECHET:8;

set r0 = min (r01,1);

A7: min (r01,1) > 0 by A5, XXREAL_0:21;

A8: min (r01,1) > 0 by A5, XXREAL_0:21;

min (r01,1) <= r01 by XXREAL_0:17;

then ( r - r01 <= r - (min (r01,1)) & r + (min (r01,1)) <= r + r01 ) by XREAL_1:6, XREAL_1:10;

then ].(r - (min (r01,1))),(r + (min (r01,1))).[ c= ].(r - r01),(r + r01).[ by XXREAL_1:46;

then A9: ].(r - (min (r01,1))),(r + (min (r01,1))).[ c= V by A6;

A10: ex r8 being Real st

( f1 . p = r8 & r8 >= 0 ) by A2;

A11: r = sqrt r1 by A4;

then A12: r1 = r ^2 by A10, SQUARE_1:def 2;

A13: r >= 0 by A10, A11, SQUARE_1:17, SQUARE_1:26;

then A14: ((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2) > 0 + 0 by A8, SQUARE_1:12, XREAL_1:8;

per cases
( r - (min (r01,1)) > 0 or r - (min (r01,1)) <= 0 )
;

end;

suppose A15:
r - (min (r01,1)) > 0
; :: thesis: ex W being Subset of X st

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

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

set r4 = (min (r01,1)) * (r - (min (r01,1)));

reconsider G1 = ].(r1 - ((min (r01,1)) * (r - (min (r01,1))))),(r1 + ((min (r01,1)) * (r - (min (r01,1))))).[ as Subset of R^1 by TOPMETR:17;

A16: r1 < r1 + ((min (r01,1)) * (r - (min (r01,1)))) by A8, A15, XREAL_1:29, XREAL_1:129;

then r1 - ((min (r01,1)) * (r - (min (r01,1)))) < r1 by XREAL_1:19;

then A17: f1 . p in G1 by A16, XXREAL_1:4;

G1 is open by JORDAN6:35;

then consider W1 being Subset of X such that

A18: ( p in W1 & W1 is open ) and

A19: f1 .: W1 c= G1 by A1, A17, JGRAPH_2:10;

set W = W1;

A20: ( (r - ((1 / 2) * (min (r01,1)))) ^2 >= 0 & (min (r01,1)) ^2 >= 0 ) by XREAL_1:63;

then A21: (min (r01,1)) * r > 0 by A8, XREAL_1:129;

then 0 + (r * (min (r01,1))) < (r * (min (r01,1))) + (r * (min (r01,1))) by XREAL_1:8;

then ((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1))) < ((2 * r) * (min (r01,1))) - ((min (r01,1)) * (min (r01,1))) by XREAL_1:14;

then - ((min (r01,1)) * (r - (min (r01,1)))) > - (((2 * r) * (min (r01,1))) - ((min (r01,1)) ^2)) by XREAL_1:24;

then r1 + (- ((min (r01,1)) * (r - (min (r01,1))))) > (r ^2) + (- (((2 * r) * (min (r01,1))) - ((min (r01,1)) ^2))) by A12, XREAL_1:8;

then sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > sqrt ((r - (min (r01,1))) ^2) by SQUARE_1:27, XREAL_1:63;

then A22: sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > r - (min (r01,1)) by A15, SQUARE_1:22;

0 + (r * (min (r01,1))) < (r * (min (r01,1))) + (r * (min (r01,1))) by A21, XREAL_1:8;

then ((min (r01,1)) * r) + 0 < ((2 * r) * (min (r01,1))) + (2 * ((min (r01,1)) * (min (r01,1)))) by A8, XREAL_1:8;

then (((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1)))) + ((min (r01,1)) * (min (r01,1))) < (((2 * r) * (min (r01,1))) + ((min (r01,1)) * (min (r01,1)))) + ((min (r01,1)) * (min (r01,1))) ;

then ((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1))) < ((2 * r) * (min (r01,1))) + ((min (r01,1)) * (min (r01,1))) by XREAL_1:7;

then r1 + ((min (r01,1)) * (r - (min (r01,1)))) < (r ^2) + (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) by A12, XREAL_1:8;

then sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) < sqrt ((r + (min (r01,1))) ^2) by A10, A8, A15, SQUARE_1:27;

then A23: r + (min (r01,1)) > sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) by A13, A7, SQUARE_1:22;

A24: r1 - ((min (r01,1)) * (r - (min (r01,1)))) = (r ^2) - (((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1)))) by A10, A11, SQUARE_1:def 2

.= ((r - ((1 / 2) * (min (r01,1)))) ^2) + ((3 / 4) * ((min (r01,1)) ^2)) ;

g0 .: W1 c= ].(r - (min (r01,1))),(r + (min (r01,1))).[

( p in W & W is open & g0 .: W c= V ) by A9, A18, XBOOLE_1:1; :: thesis: verum

end;reconsider G1 = ].(r1 - ((min (r01,1)) * (r - (min (r01,1))))),(r1 + ((min (r01,1)) * (r - (min (r01,1))))).[ as Subset of R^1 by TOPMETR:17;

A16: r1 < r1 + ((min (r01,1)) * (r - (min (r01,1)))) by A8, A15, XREAL_1:29, XREAL_1:129;

then r1 - ((min (r01,1)) * (r - (min (r01,1)))) < r1 by XREAL_1:19;

then A17: f1 . p in G1 by A16, XXREAL_1:4;

G1 is open by JORDAN6:35;

then consider W1 being Subset of X such that

A18: ( p in W1 & W1 is open ) and

A19: f1 .: W1 c= G1 by A1, A17, JGRAPH_2:10;

set W = W1;

A20: ( (r - ((1 / 2) * (min (r01,1)))) ^2 >= 0 & (min (r01,1)) ^2 >= 0 ) by XREAL_1:63;

now :: thesis: not r1 = 0

then
0 < r
by A10, A11, SQUARE_1:25;assume
r1 = 0
; :: thesis: contradiction

then r = 0 by A4, SQUARE_1:17;

hence contradiction by A7, A15; :: thesis: verum

end;then r = 0 by A4, SQUARE_1:17;

hence contradiction by A7, A15; :: thesis: verum

then A21: (min (r01,1)) * r > 0 by A8, XREAL_1:129;

then 0 + (r * (min (r01,1))) < (r * (min (r01,1))) + (r * (min (r01,1))) by XREAL_1:8;

then ((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1))) < ((2 * r) * (min (r01,1))) - ((min (r01,1)) * (min (r01,1))) by XREAL_1:14;

then - ((min (r01,1)) * (r - (min (r01,1)))) > - (((2 * r) * (min (r01,1))) - ((min (r01,1)) ^2)) by XREAL_1:24;

then r1 + (- ((min (r01,1)) * (r - (min (r01,1))))) > (r ^2) + (- (((2 * r) * (min (r01,1))) - ((min (r01,1)) ^2))) by A12, XREAL_1:8;

then sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > sqrt ((r - (min (r01,1))) ^2) by SQUARE_1:27, XREAL_1:63;

then A22: sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > r - (min (r01,1)) by A15, SQUARE_1:22;

0 + (r * (min (r01,1))) < (r * (min (r01,1))) + (r * (min (r01,1))) by A21, XREAL_1:8;

then ((min (r01,1)) * r) + 0 < ((2 * r) * (min (r01,1))) + (2 * ((min (r01,1)) * (min (r01,1)))) by A8, XREAL_1:8;

then (((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1)))) + ((min (r01,1)) * (min (r01,1))) < (((2 * r) * (min (r01,1))) + ((min (r01,1)) * (min (r01,1)))) + ((min (r01,1)) * (min (r01,1))) ;

then ((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1))) < ((2 * r) * (min (r01,1))) + ((min (r01,1)) * (min (r01,1))) by XREAL_1:7;

then r1 + ((min (r01,1)) * (r - (min (r01,1)))) < (r ^2) + (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) by A12, XREAL_1:8;

then sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) < sqrt ((r + (min (r01,1))) ^2) by A10, A8, A15, SQUARE_1:27;

then A23: r + (min (r01,1)) > sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) by A13, A7, SQUARE_1:22;

A24: r1 - ((min (r01,1)) * (r - (min (r01,1)))) = (r ^2) - (((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1)))) by A10, A11, SQUARE_1:def 2

.= ((r - ((1 / 2) * (min (r01,1)))) ^2) + ((3 / 4) * ((min (r01,1)) ^2)) ;

g0 .: W1 c= ].(r - (min (r01,1))),(r + (min (r01,1))).[

proof

hence
ex W being Subset of X st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: W1 or x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ )

assume x in g0 .: W1 ; :: thesis: x in ].(r - (min (r01,1))),(r + (min (r01,1))).[

then consider z being object such that

A25: z in dom g0 and

A26: z in W1 and

A27: g0 . z = x by FUNCT_1:def 6;

reconsider pz = z as Point of X by A25;

reconsider aa1 = f1 . pz as Real ;

A28: ex r9 being Real st

( f1 . pz = r9 & r9 >= 0 ) by A2;

pz in the carrier of X ;

then pz in dom f1 by FUNCT_2:def 1;

then A29: f1 . pz in f1 .: W1 by A26, FUNCT_1:def 6;

then aa1 < r1 + ((min (r01,1)) * (r - (min (r01,1)))) by A19, XXREAL_1:4;

then sqrt aa1 < sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) by A28, SQUARE_1:27;

then A30: sqrt aa1 < r + (min (r01,1)) by A23, XXREAL_0:2;

A31: r1 - ((min (r01,1)) * (r - (min (r01,1)))) < aa1 by A19, A29, XXREAL_1:4;

hence x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ by A30, A32, XXREAL_1:4; :: thesis: verum

end;assume x in g0 .: W1 ; :: thesis: x in ].(r - (min (r01,1))),(r + (min (r01,1))).[

then consider z being object such that

A25: z in dom g0 and

A26: z in W1 and

A27: g0 . z = x by FUNCT_1:def 6;

reconsider pz = z as Point of X by A25;

reconsider aa1 = f1 . pz as Real ;

A28: ex r9 being Real st

( f1 . pz = r9 & r9 >= 0 ) by A2;

pz in the carrier of X ;

then pz in dom f1 by FUNCT_2:def 1;

then A29: f1 . pz in f1 .: W1 by A26, FUNCT_1:def 6;

then aa1 < r1 + ((min (r01,1)) * (r - (min (r01,1)))) by A19, XXREAL_1:4;

then sqrt aa1 < sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) by A28, SQUARE_1:27;

then A30: sqrt aa1 < r + (min (r01,1)) by A23, XXREAL_0:2;

A31: r1 - ((min (r01,1)) * (r - (min (r01,1)))) < aa1 by A19, A29, XXREAL_1:4;

A32: now :: thesis: ( ( 0 <= r1 - ((min (r01,1)) * (r - (min (r01,1)))) & r - (min (r01,1)) < sqrt aa1 ) or ( 0 > r1 - ((min (r01,1)) * (r - (min (r01,1)))) & contradiction ) )end;

x = sqrt aa1
by A4, A27;per cases
( 0 <= r1 - ((min (r01,1)) * (r - (min (r01,1)))) or 0 > r1 - ((min (r01,1)) * (r - (min (r01,1)))) )
;

end;

case
0 <= r1 - ((min (r01,1)) * (r - (min (r01,1))))
; :: thesis: r - (min (r01,1)) < sqrt aa1

then
sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) <= sqrt aa1
by A31, SQUARE_1:26;

hence r - (min (r01,1)) < sqrt aa1 by A22, XXREAL_0:2; :: thesis: verum

end;hence r - (min (r01,1)) < sqrt aa1 by A22, XXREAL_0:2; :: thesis: verum

hence x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ by A30, A32, XXREAL_1:4; :: thesis: verum

( p in W & W is open & g0 .: W c= V ) by A9, A18, XBOOLE_1:1; :: thesis: verum

suppose A33:
r - (min (r01,1)) <= 0
; :: thesis: ex W being Subset of X st

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

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

set r4 = (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3;

reconsider G1 = ].(r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)),(r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)).[ as Subset of R^1 by TOPMETR:17;

(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3 > 0 by A14, XREAL_1:139;

then A34: r1 < r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) by XREAL_1:29;

then r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < r1 by XREAL_1:19;

then A35: f1 . p in G1 by A34, XXREAL_1:4;

G1 is open by JORDAN6:35;

then consider W1 being Subset of X such that

A36: ( p in W1 & W1 is open ) and

A37: f1 .: W1 c= G1 by A1, A35, JGRAPH_2:10;

set W = W1;

(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3 < ((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2) by A14, XREAL_1:221;

then r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < (r ^2) + (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) by A12, XREAL_1:8;

then sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) <= sqrt ((r + (min (r01,1))) ^2) by A10, A13, A8, SQUARE_1:26;

then A38: r + (min (r01,1)) >= sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) by A13, A7, SQUARE_1:22;

g0 .: W1 c= ].(r - (min (r01,1))),(r + (min (r01,1))).[

( p in W & W is open & g0 .: W c= V ) by A9, A36, XBOOLE_1:1; :: thesis: verum

end;reconsider G1 = ].(r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)),(r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)).[ as Subset of R^1 by TOPMETR:17;

(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3 > 0 by A14, XREAL_1:139;

then A34: r1 < r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) by XREAL_1:29;

then r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < r1 by XREAL_1:19;

then A35: f1 . p in G1 by A34, XXREAL_1:4;

G1 is open by JORDAN6:35;

then consider W1 being Subset of X such that

A36: ( p in W1 & W1 is open ) and

A37: f1 .: W1 c= G1 by A1, A35, JGRAPH_2:10;

set W = W1;

(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3 < ((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2) by A14, XREAL_1:221;

then r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < (r ^2) + (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) by A12, XREAL_1:8;

then sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) <= sqrt ((r + (min (r01,1))) ^2) by A10, A13, A8, SQUARE_1:26;

then A38: r + (min (r01,1)) >= sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) by A13, A7, SQUARE_1:22;

g0 .: W1 c= ].(r - (min (r01,1))),(r + (min (r01,1))).[

proof

hence
ex W being Subset of X st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: W1 or x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ )

assume x in g0 .: W1 ; :: thesis: x in ].(r - (min (r01,1))),(r + (min (r01,1))).[

then consider z being object such that

A39: z in dom g0 and

A40: z in W1 and

A41: g0 . z = x by FUNCT_1:def 6;

reconsider pz = z as Point of X by A39;

reconsider aa1 = f1 . pz as Real ;

A42: ex r9 being Real st

( f1 . pz = r9 & r9 >= 0 ) by A2;

pz in the carrier of X ;

then pz in dom f1 by FUNCT_2:def 1;

then A43: f1 . pz in f1 .: W1 by A40, FUNCT_1:def 6;

then aa1 < r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) by A37, XXREAL_1:4;

then sqrt aa1 < sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) by A42, SQUARE_1:27;

then A44: sqrt aa1 < r + (min (r01,1)) by A38, XXREAL_0:2;

A45: r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < aa1 by A37, A43, XXREAL_1:4;

hence x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ by A44, A46, XXREAL_1:4; :: thesis: verum

end;assume x in g0 .: W1 ; :: thesis: x in ].(r - (min (r01,1))),(r + (min (r01,1))).[

then consider z being object such that

A39: z in dom g0 and

A40: z in W1 and

A41: g0 . z = x by FUNCT_1:def 6;

reconsider pz = z as Point of X by A39;

reconsider aa1 = f1 . pz as Real ;

A42: ex r9 being Real st

( f1 . pz = r9 & r9 >= 0 ) by A2;

pz in the carrier of X ;

then pz in dom f1 by FUNCT_2:def 1;

then A43: f1 . pz in f1 .: W1 by A40, FUNCT_1:def 6;

then aa1 < r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) by A37, XXREAL_1:4;

then sqrt aa1 < sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) by A42, SQUARE_1:27;

then A44: sqrt aa1 < r + (min (r01,1)) by A38, XXREAL_0:2;

A45: r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < aa1 by A37, A43, XXREAL_1:4;

A46: now :: thesis: ( ( r - (min (r01,1)) = 0 & r - (min (r01,1)) < sqrt aa1 ) or ( r - (min (r01,1)) < 0 & r - (min (r01,1)) < sqrt aa1 ) )

x = sqrt aa1
by A4, A41;end;

hence x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ by A44, A46, XXREAL_1:4; :: thesis: verum

( p in W & W is open & g0 .: W c= V ) by A9, A36, XBOOLE_1:1; :: thesis: verum

for p being Point of X

for r11 being Real st f1 . p = r11 holds

g0 . p = sqrt r11 by A4;

hence ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous ) by A47; :: thesis: verum