reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:19;
reconsider f = Sq_Circ as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A1: for p being Point of ((TOP-REAL 2) | D) holds f . p <> f . (0. (TOP-REAL 2))
proof
let p be Point of ((TOP-REAL 2) | D); :: thesis: f . p <> f . (0. (TOP-REAL 2))
A2: [#] ((TOP-REAL 2) | D) = D by PRE_TOPC:def 10;
then reconsider q = p as Point of (TOP-REAL 2) by XBOOLE_0:def 5;
not p in {(0. (TOP-REAL 2))} by A2, XBOOLE_0:def 5;
then A3: not p = 0. (TOP-REAL 2) by TARSKI:def 1;
per cases ( ( not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) or ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ;
suppose A4: ( not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: f . p <> f . (0. (TOP-REAL 2))
A5: q `2 <> 0 by A4;
set q9 = |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]|;
A6: |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| `2 = (q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) by EUCLID:56;
A7: sqrt (1 + (((q `1 ) / (q `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A8: now
assume |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then 0 * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) = ((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) by A6, EUCLID:56, EUCLID:58;
hence contradiction by A5, A7, XCMPLX_1:88; :: thesis: verum
end;
Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| by A3, A4, Def1;
hence f . p <> f . (0. (TOP-REAL 2)) by A8, Def1; :: thesis: verum
end;
suppose A9: ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: f . p <> f . (0. (TOP-REAL 2))
set q9 = |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]|;
A12: |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| `1 = (q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) by EUCLID:56;
A13: sqrt (1 + (((q `2 ) / (q `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A14: now
assume |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then 0 * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) = ((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) by A12, EUCLID:56, EUCLID:58;
hence contradiction by A10, A13, XCMPLX_1:88; :: thesis: verum
end;
Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| by A3, A9, Def1;
hence f . p <> f . (0. (TOP-REAL 2)) by A14, Def1; :: thesis: verum
end;
end;
end;
A15: f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2) by Def1;
A16: for V being Subset of (TOP-REAL 2) st f . (0. (TOP-REAL 2)) in V & V is open holds
ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V )
proof
reconsider u0 = 0. (TOP-REAL 2) as Point of (Euclid 2) by EUCLID:71;
let V be Subset of (TOP-REAL 2); :: thesis: ( f . (0. (TOP-REAL 2)) in V & V is open implies ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V ) )
reconsider VV = V as Subset of (TopSpaceMetr (Euclid 2)) by Lm16;
assume that
A17: f . (0. (TOP-REAL 2)) in V and
A18: V is open ; :: thesis: ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V )
VV is open by A18, Lm16, PRE_TOPC:60;
then consider r being real number such that
A19: r > 0 and
A20: Ball u0,r c= V by A15, A17, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
reconsider W1 = Ball u0,r as Subset of (TOP-REAL 2) by EUCLID:71;
A21: W1 is open by GOBOARD6:6;
A22: f .: W1 c= W1
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in f .: W1 or z in W1 )
assume z in f .: W1 ; :: thesis: z in W1
then consider y being set such that
A23: y in dom f and
A24: y in W1 and
A25: z = f . y by FUNCT_1:def 12;
z in rng f by A23, A25, FUNCT_1:def 5;
then reconsider qz = z as Point of (TOP-REAL 2) ;
reconsider pz = qz as Point of (Euclid 2) by EUCLID:71;
reconsider q = y as Point of (TOP-REAL 2) by A23;
reconsider qy = q as Point of (Euclid 2) by EUCLID:71;
dist u0,qy < r by A24, METRIC_1:12;
then |.((0. (TOP-REAL 2)) - q).| < r by JGRAPH_1:45;
then sqrt (((((0. (TOP-REAL 2)) - q) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - q) `2 ) ^2 )) < r by JGRAPH_1:47;
then sqrt (((((0. (TOP-REAL 2)) `1 ) - (q `1 )) ^2 ) + ((((0. (TOP-REAL 2)) - q) `2 ) ^2 )) < r by TOPREAL3:8;
then A26: sqrt (((((0. (TOP-REAL 2)) `1 ) - (q `1 )) ^2 ) + ((((0. (TOP-REAL 2)) `2 ) - (q `2 )) ^2 )) < r by TOPREAL3:8;
per cases ( q = 0. (TOP-REAL 2) or ( q <> 0. (TOP-REAL 2) & ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ) or ( q <> 0. (TOP-REAL 2) & not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ) ;
suppose A27: ( q <> 0. (TOP-REAL 2) & ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ) ; :: thesis: z in W1
A28: (q `2 ) ^2 >= 0 by XREAL_1:65;
((q `2 ) / (q `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((q `2 ) / (q `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A29: sqrt (1 + (((q `2 ) / (q `1 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
then (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 >= sqrt (1 + (((q `2 ) / (q `1 )) ^2 )) by XREAL_1:153;
then A30: 1 <= (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 by A29, XXREAL_0:2;
A31: Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| by A27, Def1;
then (qz `2 ) ^2 = ((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) ^2 by A25, EUCLID:56
.= ((q `2 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 ) by XCMPLX_1:77 ;
then A32: (qz `2 ) ^2 <= ((q `2 ) ^2 ) / 1 by A30, A28, XREAL_1:120;
A33: (q `1 ) ^2 >= 0 by XREAL_1:65;
(qz `1 ) ^2 = ((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) ^2 by A25, A31, EUCLID:56
.= ((q `1 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 ) by XCMPLX_1:77 ;
then (qz `1 ) ^2 <= ((q `1 ) ^2 ) / 1 by A30, A33, XREAL_1:120;
then A34: ((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by A32, XREAL_1:9;
( (qz `1 ) ^2 >= 0 & (qz `2 ) ^2 >= 0 ) by XREAL_1:65;
then A35: sqrt (((qz `1 ) ^2 ) + ((qz `2 ) ^2 )) <= sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 )) by A34, SQUARE_1:94;
A36: ((0. (TOP-REAL 2)) - qz) `2 = ((0. (TOP-REAL 2)) `2 ) - (qz `2 ) by TOPREAL3:8
.= - (qz `2 ) by JGRAPH_2:11 ;
((0. (TOP-REAL 2)) - qz) `1 = ((0. (TOP-REAL 2)) `1 ) - (qz `1 ) by TOPREAL3:8
.= - (qz `1 ) by JGRAPH_2:11 ;
then sqrt (((((0. (TOP-REAL 2)) - qz) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `2 ) ^2 )) < r by A26, A36, A35, JGRAPH_2:11, XXREAL_0:2;
then |.((0. (TOP-REAL 2)) - qz).| < r by JGRAPH_1:47;
then dist u0,pz < r by JGRAPH_1:45;
hence z in W1 by METRIC_1:12; :: thesis: verum
end;
suppose A37: ( q <> 0. (TOP-REAL 2) & not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: z in W1
A38: (q `2 ) ^2 >= 0 by XREAL_1:65;
((q `1 ) / (q `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((q `1 ) / (q `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A39: sqrt (1 + (((q `1 ) / (q `2 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
then (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 >= sqrt (1 + (((q `1 ) / (q `2 )) ^2 )) by XREAL_1:153;
then A40: 1 <= (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 by A39, XXREAL_0:2;
A41: Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| by A37, Def1;
then (qz `2 ) ^2 = ((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) ^2 by A25, EUCLID:56
.= ((q `2 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 ) by XCMPLX_1:77 ;
then A42: (qz `2 ) ^2 <= ((q `2 ) ^2 ) / 1 by A40, A38, XREAL_1:120;
A43: (q `1 ) ^2 >= 0 by XREAL_1:65;
(qz `1 ) ^2 = ((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) ^2 by A25, A41, EUCLID:56
.= ((q `1 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 ) by XCMPLX_1:77 ;
then (qz `1 ) ^2 <= ((q `1 ) ^2 ) / 1 by A40, A43, XREAL_1:120;
then A44: ((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by A42, XREAL_1:9;
( (qz `1 ) ^2 >= 0 & (qz `2 ) ^2 >= 0 ) by XREAL_1:65;
then A45: sqrt (((qz `1 ) ^2 ) + ((qz `2 ) ^2 )) <= sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 )) by A44, SQUARE_1:94;
A46: ((0. (TOP-REAL 2)) - qz) `2 = ((0. (TOP-REAL 2)) `2 ) - (qz `2 ) by TOPREAL3:8
.= - (qz `2 ) by JGRAPH_2:11 ;
((0. (TOP-REAL 2)) - qz) `1 = ((0. (TOP-REAL 2)) `1 ) - (qz `1 ) by TOPREAL3:8
.= - (qz `1 ) by JGRAPH_2:11 ;
then sqrt (((((0. (TOP-REAL 2)) - qz) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `2 ) ^2 )) < r by A26, A46, A45, JGRAPH_2:11, XXREAL_0:2;
then |.((0. (TOP-REAL 2)) - qz).| < r by JGRAPH_1:47;
then dist u0,pz < r by JGRAPH_1:45;
hence z in W1 by METRIC_1:12; :: thesis: verum
end;
end;
end;
u0 in W1 by A19, GOBOARD6:4;
hence ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V ) by A20, A21, A22, XBOOLE_1:1; :: thesis: verum
end;
A47: D ` = {(0. (TOP-REAL 2))} by Th30;
then ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous ) by Th29;
hence ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = Sq_Circ & h is continuous ) by A15, A47, A1, A16, Th13; :: thesis: verum