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 number 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 number 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 number 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 number st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous ) )
assume A1: ( f1 is continuous & ( for q being Point of X ex r being real number 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 number st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous )
defpred S1[ set , set ] means for r11 being real number st f1 . $1 = r11 holds
$2 = sqrt r11;
A2: 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 pp = x as Point of X ;
reconsider r1 = f1 . pp as Real by TOPMETR:24;
for r11 being real number st f1 . x = r11 holds
sqrt r1 = sqrt r11 ;
hence ex y being Element of REAL st 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 FUNCT_2:sch 3(A2);
 then consider f being Function of the carrier of X, REAL such that
A3: for x2 being Element of X
for r11 being real number st f1 . x2 = r11 holds
f . x2 = sqrt r11 ;
reconsider g0 = f as Function of X,R^1 by TOPMETR:24;
A4: for p being Point of X
for r11 being real number st f1 . p = r11 holds
g0 . p = sqrt r11 by A3;
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 ) )
assume A5: ( 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 )
reconsider r = g0 . p as Real by TOPMETR:24;
reconsider r1 = f1 . p as Real by TOPMETR:24;
consider r8 being real number such that
A6: ( f1 . p = r8 & r8 >= 0 ) by A1;
A7: r = sqrt r1 by A3;
then A8: r >= 0 by A6, SQUARE_1:82, SQUARE_1:94;
consider r01 being Real such that
A9: ( r01 > 0 & ].(r - r01),(r + r01).[ c= V ) by A5, FRECHET:8;
set r0 = min r01,1;
A10: min r01,1 > 0 by A9, XXREAL_0:21;
A11: r1 = r ^2 by A6, A7, SQUARE_1:def 4;
A12: r + (min r01,1) >= r + 0 by A10, XREAL_1:9;
min r01,1 <= r01 by XXREAL_0:17;
then ( r - r01 <= r - (min r01,1) & r + (min r01,1) <= r + r01 ) by XREAL_1:8, XREAL_1:12;
then ].(r - (min r01,1)),(r + (min r01,1)).[ c= ].(r - r01),(r + r01).[ by XXREAL_1:46;
then A13: ( min r01,1 > 0 & ].(r - (min r01,1)),(r + (min r01,1)).[ c= V ) by A9, XXREAL_0:21, XBOOLE_1:1;
2 * r >= 0 by A8;
then (2 * r) * (min r01,1) >= 0 by A13;
then A14: ((2 * r) * (min r01,1)) + ((min r01,1) ^2 ) > 0 + 0 by A13, SQUARE_1:74, XREAL_1:10;
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 )
now
assume r1 = 0 ; :: thesis: contradiction
then r = 0 by A3, SQUARE_1:82;
then - (min r01,1) > 0 by A15;
hence contradiction by A10; :: thesis: verum
end;
then A16: 0 < r by A6, A7, SQUARE_1:93;
set r4 = (min r01,1) * (r - (min r01,1));
A17: (min r01,1) * (r - (min r01,1)) > 0 by A13, A15, XREAL_1:131;
then A18: r1 + ((min r01,1) * (r - (min r01,1))) > 0 + 0 by A6;
(min r01,1) * (min r01,1) > 0 by A13, XREAL_1:131;
then A19: 2 * ((min r01,1) * (min r01,1)) > 0 by XREAL_1:131;
A20: (min r01,1) * r > 0 by A13, A16, XREAL_1:131;
then 0 + (r * (min r01,1)) < (r * (min r01,1)) + (r * (min r01,1)) by XREAL_1:10;
then ((min r01,1) * r) + 0 < ((2 * r) * (min r01,1)) + (2 * ((min r01,1) * (min r01,1))) by A19, XREAL_1:10;
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:9;
then r1 + ((min r01,1) * (r - (min r01,1))) < (r ^2 ) + (((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) by A11, XREAL_1:10;
then sqrt (r1 + ((min r01,1) * (r - (min r01,1)))) < sqrt ((r + (min r01,1)) ^2 ) by A18, SQUARE_1:95;
then A21: r + (min r01,1) > sqrt (r1 + ((min r01,1) * (r - (min r01,1)))) by A8, A12, SQUARE_1:89;
0 + (r * (min r01,1)) < (r * (min r01,1)) + (r * (min r01,1)) by A20, XREAL_1:10;
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:16;
then - ((min r01,1) * (r - (min r01,1))) > - (((2 * r) * (min r01,1)) - ((min r01,1) ^2 )) by XREAL_1:26;
then r1 + (- ((min r01,1) * (r - (min r01,1)))) > (r ^2 ) + (- (((2 * r) * (min r01,1)) - ((min r01,1) ^2 ))) by A11, XREAL_1:10;
then sqrt (r1 - ((min r01,1) * (r - (min r01,1)))) > sqrt ((r - (min r01,1)) ^2 ) by SQUARE_1:95, XREAL_1:65;
then A22: sqrt (r1 - ((min r01,1) * (r - (min r01,1)))) > r - (min r01,1) by A15, SQUARE_1:89;
A23: r1 - ((min r01,1) * (r - (min r01,1))) = (r ^2 ) - (((min r01,1) * r) - ((min r01,1) * (min r01,1))) by A6, A7, SQUARE_1:def 4
.= ((r - ((1 / 2) * (min r01,1))) ^2 ) + ((3 / 4) * ((min r01,1) ^2 )) ;
A24: (r - ((1 / 2) * (min r01,1))) ^2 >= 0 by XREAL_1:65;
(min r01,1) ^2 >= 0 by XREAL_1:65;
then (3 / 4) * ((min r01,1) ^2 ) >= 0 ;
then A25: r1 - ((min r01,1) * (r - (min r01,1))) >= 0 + 0 by A23, A24;
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:24;
A26: r1 < r1 + ((min r01,1) * (r - (min r01,1))) by A17, XREAL_1:31;
then r1 - ((min r01,1) * (r - (min r01,1))) < r1 by XREAL_1:21;
then A27: f1 . p in G1 by A26, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A28: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A27, JGRAPH_2:20;
set W = W1;
g0 .: W1 c= ].(r - (min r01,1)),(r + (min r01,1)).[
proof
let x be set ; :: 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 set such that
A29: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A29;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A30: f1 . pz in f1 .: W1 by A29, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
consider r9 being real number such that
A31: ( f1 . pz = r9 & r9 >= 0 ) by A1;
A32: x = sqrt aa1 by A3, A29;
A33: ( r1 - ((min r01,1) * (r - (min r01,1))) < aa1 & aa1 < r1 + ((min r01,1) * (r - (min r01,1))) ) by A28, A30, XXREAL_1:4;
then sqrt aa1 < sqrt (r1 + ((min r01,1) * (r - (min r01,1)))) by A31, SQUARE_1:95;
then A34: sqrt aa1 < r + (min r01,1) by A21, XXREAL_0:2;
now
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 A33, SQUARE_1:94;
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 A25; :: thesis: verum
end;
end;
end;
hence x in ].(r - (min r01,1)),(r + (min r01,1)).[ by A32, A34, 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 A13, A28, XBOOLE_1:1; :: thesis: verum
end;
suppose A35: 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;
A36: (((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3 > 0 by A14, XREAL_1:141;
then A37: r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) > 0 + 0 by A6;
(((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3 < ((2 * r) * (min r01,1)) + ((min r01,1) ^2 ) by A14, XREAL_1:223;
then r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) < (r ^2 ) + (((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) by A11, XREAL_1:10;
then sqrt (r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3)) <= sqrt ((r + (min r01,1)) ^2 ) by A37, SQUARE_1:94;
then A38: r + (min r01,1) >= sqrt (r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3)) by A8, A12, SQUARE_1:89;
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:24;
A39: r1 < r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) by A36, XREAL_1:31;
then r1 - ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) < r1 by XREAL_1:21;
then A40: f1 . p in G1 by A39, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A41: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A40, JGRAPH_2:20;
set W = W1;
g0 .: W1 c= ].(r - (min r01,1)),(r + (min r01,1)).[
proof
let x be set ; :: 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 set such that
A42: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A42;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A43: f1 . pz in f1 .: W1 by A42, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
consider r9 being real number such that
A44: ( f1 . pz = r9 & r9 >= 0 ) by A1;
A45: x = sqrt aa1 by A3, A42;
A46: ( r1 - ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) < aa1 & aa1 < r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) ) by A41, A43, XXREAL_1:4;
then sqrt aa1 < sqrt (r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3)) by A44, SQUARE_1:95;
then A47: sqrt aa1 < r + (min r01,1) by A38, XXREAL_0:2;
now
per cases ( r - (min r01,1) = 0 or r - (min r01,1) < 0 ) by A35;
case r - (min r01,1) = 0 ; :: thesis: r - (min r01,1) < sqrt aa1
hence r - (min r01,1) < sqrt aa1 by A11, A46, SQUARE_1:82, SQUARE_1:95; :: thesis: verum
end;
case r - (min r01,1) < 0 ; :: thesis: r - (min r01,1) < sqrt aa1
hence r - (min r01,1) < sqrt aa1 by A44, SQUARE_1:82, SQUARE_1:94; :: thesis: verum
end;
end;
end;
hence x in ].(r - (min r01,1)),(r + (min r01,1)).[ by A45, A47, 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 A13, A41, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
then g0 is continuous by JGRAPH_2:20;
hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous ) by A4; :: thesis: verum