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 S1[ 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 S1[x,y]
proof
let x be Element of X; :: thesis: ex y being Element of REAL st S1[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: S1[x,y]
thus S1[x,y] ; :: thesis: verum
end;
ex f being Function of the carrier of X,REAL st
for x2 being Element of X holds S1[x2,f . x2] from 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 ;
A8: min (r01,1) > 0 by ;
min (r01,1) <= r01 by XXREAL_0:17;
then ( r - r01 <= r - (min (r01,1)) & r + (min (r01,1)) <= r + r01 ) by ;
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 ;
A13: r >= 0 by ;
then A14: ((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2) > 0 + 0 by ;
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 ;
then r1 - ((min (r01,1)) * (r - (min (r01,1)))) < r1 by XREAL_1:19;
then A17: f1 . p in G1 by ;
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 ;
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 ;
hence contradiction by A7, A15; :: thesis: verum
end;
then 0 < r by ;
then A21: (min (r01,1)) * r > 0 by ;
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 ;
then sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > sqrt ((r - (min (r01,1))) ^2) by ;
then A22: sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > r - (min (r01,1)) by ;
0 + (r * (min (r01,1))) < (r * (min (r01,1))) + (r * (min (r01,1))) by ;
then ((min (r01,1)) * r) + 0 < ((2 * r) * (min (r01,1))) + (2 * ((min (r01,1)) * (min (r01,1)))) by ;
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 ;
then sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) < sqrt ((r + (min (r01,1))) ^2) by ;
then A23: r + (min (r01,1)) > sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) by ;
A24: r1 - ((min (r01,1)) * (r - (min (r01,1)))) = (r ^2) - (((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1)))) by
.= ((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 ;
then aa1 < r1 + ((min (r01,1)) * (r - (min (r01,1)))) by ;
then sqrt aa1 < sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) by ;
then A30: sqrt aa1 < r + (min (r01,1)) by ;
A31: r1 - ((min (r01,1)) * (r - (min (r01,1)))) < aa1 by ;
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 ;
hence r - (min (r01,1)) < sqrt aa1 by ; :: thesis: verum
end;
case 0 > r1 - ((min (r01,1)) * (r - (min (r01,1)))) ; :: thesis: contradiction
end;
end;
end;
x = sqrt aa1 by ;
hence x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ by ; :: thesis: verum
end;
hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by ; :: 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 ;
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 ;
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 ;
set W = W1;
(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3 < ((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2) by ;
then r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < (r ^2) + (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) by ;
then sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) <= sqrt ((r + (min (r01,1))) ^2) by ;
then A38: r + (min (r01,1)) >= sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) by ;
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 ;
then aa1 < r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) by ;
then sqrt aa1 < sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) by ;
then A44: sqrt aa1 < r + (min (r01,1)) by ;
A45: r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < aa1 by ;
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 ; :: thesis: verum
end;
case r - (min (r01,1)) < 0 ; :: thesis: r - (min (r01,1)) < sqrt aa1
hence r - (min (r01,1)) < sqrt aa1 by ; :: thesis: verum
end;
end;
end;
x = sqrt aa1 by ;
hence x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ by ; :: thesis: verum
end;
hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by ; :: 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