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₁[ 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₁[x,y]

proof

let x be Element of X; :: thesis: ex y being Element of REAL st S₁[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₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

ex f being Function of the carrier of X,REAL st
for x2 being Element of X holds S₁[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 )

proof

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;

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

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 )

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;

now :: thesis: not r1 = 0

assume r1 = 0 ; :: thesis: contradiction
then r = 0 by A4, SQUARE_1:17;
hence contradiction by A7, A15; :: thesis: verum

end;

then 0 < r by A10, A11, SQUARE_1:25;
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

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;

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

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

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;

case 0 > r1 - ((min (r01,1)) * (r - (min (r01,1)))) ; :: thesis: contradiction

hence contradiction by A24, A20; :: thesis: verum

end;

end;

end;

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

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A9, A18, XBOOLE_1:1; :: thesis: verum

end;

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 )

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))).[

proof

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;

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

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

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

hence r - (min (r01,1)) < sqrt aa1 by A12, A45, SQUARE_1:17, SQUARE_1:27; :: thesis: verum

end;

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

hence r - (min (r01,1)) < sqrt aa1 by A42, SQUARE_1:17, SQUARE_1:26; :: thesis: verum

end;

end;

end;

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

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A9, A36, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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