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 that
A1: f1 is continuous and
A2: 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;
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 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(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 number st f1 . x2 = r11 holds
f . x2 = sqrt r11 ;
reconsider g0 = f as Function of X,R^1 by TOPMETR:24;
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 by TOPMETR:24;
reconsider r1 = f1 . p as Real by TOPMETR:24;
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:8, XREAL_1:12;
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, XBOOLE_1:1;
A10: ex r8 being real number st
( f1 . p = r8 & r8 >= 0 ) by A2;
A11: r = sqrt r1 by A4;
then A12: r1 = r ^2 by A10, SQUARE_1:def 4;
A13: r >= 0 by A10, A11, SQUARE_1:82, SQUARE_1:94;
then A14: ((2 * r) * (min r01,1)) + ((min r01,1) ^2 ) > 0 + 0 by A8, 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 )
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:24;
A16: r1 < r1 + ((min r01,1) * (r - (min r01,1))) by A8, A15, XREAL_1:31, XREAL_1:131;
then r1 - ((min r01,1) * (r - (min r01,1))) < r1 by XREAL_1:21;
then A17: f1 . p in G1 by A16, XXREAL_1:4;
G1 is open by JORDAN6:46;
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:20;
set W = W1;
A20: ( (r - ((1 / 2) * (min r01,1))) ^2 >= 0 & (min r01,1) ^2 >= 0 ) by XREAL_1:65;
then 0 < r by A10, A11, SQUARE_1:93;
then A21: (min r01,1) * r > 0 by A8, 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) - ((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 A12, 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;
0 + (r * (min r01,1)) < (r * (min r01,1)) + (r * (min r01,1)) by A21, XREAL_1:10;
then ((min r01,1) * r) + 0 < ((2 * r) * (min r01,1)) + (2 * ((min r01,1) * (min r01,1))) by A8, 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 A12, XREAL_1:10;
then sqrt (r1 + ((min r01,1) * (r - (min r01,1)))) < sqrt ((r + (min r01,1)) ^2 ) by A10, A8, A15, SQUARE_1:95;
then A23: r + (min r01,1) > sqrt (r1 + ((min r01,1) * (r - (min r01,1)))) by A13, A7, SQUARE_1:89;
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 4
.= ((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 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
A25: z in dom g0 and
A26: z in W1 and
A27: g0 . z = x by FUNCT_1:def 12;
reconsider pz = z as Point of X by A25;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A28: ex r9 being real number 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 12;
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:95;
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
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: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 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:24;
(((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3 > 0 by A14, XREAL_1:141;
then A34: r1 < r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) by XREAL_1:31;
then r1 - ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3) < r1 by XREAL_1:21;
then A35: f1 . p in G1 by A34, XXREAL_1:4;
G1 is open by JORDAN6:46;
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:20;
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: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 A12, XREAL_1:10;
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:94;
then A38: r + (min r01,1) >= sqrt (r1 + ((((2 * r) * (min r01,1)) + ((min r01,1) ^2 )) / 3)) by A13, A7, SQUARE_1:89;
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
A39: z in dom g0 and
A40: z in W1 and
A41: g0 . z = x by FUNCT_1:def 12;
reconsider pz = z as Point of X by A39;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A42: ex r9 being real number 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 12;
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:95;
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
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: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 A42, SQUARE_1:82, SQUARE_1:94; :: 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:20;
for p being Point of X
for r11 being real number 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 number st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous ) by A47; :: thesis: verum