reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:9;
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 5;
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))

then A5: q `2 <> 0 ;
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:52;
A7: sqrt (1 + (((q `1) / (q `2)) ^2)) > 0 by Lm1, SQUARE_1:25;

A8: now :: thesis: not |[((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2))))]| = 0. (TOP-REAL 2)

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:52, EUCLID:54;
hence contradiction by A5, A7, XCMPLX_1:87; :: 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))

A10: now :: thesis: not q `1 = 0

assume A11: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A9;
hence contradiction by A3, A11, EUCLID:53, EUCLID:54; :: thesis: verum

end;

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:52;
A13: sqrt (1 + (((q `2) / (q `1)) ^2)) > 0 by Lm1, SQUARE_1:25;

A14: now :: thesis: not |[((q `1) / (sqrt (1 + (((q `2) / (q `1)) ^2)))),((q `2) / (sqrt (1 + (((q `2) / (q `1)) ^2))))]| = 0. (TOP-REAL 2)

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:52, EUCLID:54;
hence contradiction by A10, A13, XCMPLX_1:87; :: 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:67;
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:30;
then consider r being Real such that
A19: r > 0 and
A20: Ball (u0,r) c= V by A15, A17, TOPMETR:15;
reconsider r = r as Real ;
reconsider W1 = Ball (u0,r) as Subset of (TOP-REAL 2) by EUCLID:67;
A21: W1 is open by GOBOARD6:3;
A22: f .: W1 c= W1

proof

let z be object ; :: 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 object such that
A23: y in dom f and
A24: y in W1 and
A25: z = f . y by FUNCT_1:def 6;
z in rng f by A23, A25, FUNCT_1:def 3;
then reconsider qz = z as Point of (TOP-REAL 2) ;
reconsider pz = qz as Point of (Euclid 2) by EUCLID:67;
reconsider q = y as Point of (TOP-REAL 2) by A23;
reconsider qy = q as Point of (Euclid 2) by EUCLID:67;
dist (u0,qy) < r by A24, METRIC_1:11;
then |.((0. (TOP-REAL 2)) - q).| < r by JGRAPH_1:28;
then sqrt (((((0. (TOP-REAL 2)) - q) `1) ^2) + ((((0. (TOP-REAL 2)) - q) `2) ^2)) < r by JGRAPH_1:30;
then sqrt (((((0. (TOP-REAL 2)) `1) - (q `1)) ^2) + ((((0. (TOP-REAL 2)) - q) `2) ^2)) < r by TOPREAL3:3;
then A26: sqrt (((((0. (TOP-REAL 2)) `1) - (q `1)) ^2) + ((((0. (TOP-REAL 2)) `2) - (q `2)) ^2)) < r by TOPREAL3:3;

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 q = 0. (TOP-REAL 2) ; :: thesis: z in W1

hence z in W1 by A24, A25, Def1; :: thesis: verum

end;

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:63;
((q `2) / (q `1)) ^2 >= 0 by XREAL_1:63;
then 1 + (((q `2) / (q `1)) ^2) >= 1 + 0 by XREAL_1:7;
then A29: sqrt (1 + (((q `2) / (q `1)) ^2)) >= 1 by SQUARE_1:18, SQUARE_1:26;
then (sqrt (1 + (((q `2) / (q `1)) ^2))) ^2 >= sqrt (1 + (((q `2) / (q `1)) ^2)) by XREAL_1:151;
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:52
.= ((q `2) ^2) / ((sqrt (1 + (((q `2) / (q `1)) ^2))) ^2) by XCMPLX_1:76 ;
then A32: (qz `2) ^2 <= ((q `2) ^2) / 1 by A30, A28, XREAL_1:118;
A33: (q `1) ^2 >= 0 by XREAL_1:63;
(qz `1) ^2 = ((q `1) / (sqrt (1 + (((q `2) / (q `1)) ^2)))) ^2 by A25, A31, EUCLID:52
.= ((q `1) ^2) / ((sqrt (1 + (((q `2) / (q `1)) ^2))) ^2) by XCMPLX_1:76 ;
then (qz `1) ^2 <= ((q `1) ^2) / 1 by A30, A33, XREAL_1:118;
then A34: ((qz `1) ^2) + ((qz `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) by A32, XREAL_1:7;
( (qz `1) ^2 >= 0 & (qz `2) ^2 >= 0 ) by XREAL_1:63;
then A35: sqrt (((qz `1) ^2) + ((qz `2) ^2)) <= sqrt (((q `1) ^2) + ((q `2) ^2)) by A34, SQUARE_1:26;
A36: ((0. (TOP-REAL 2)) - qz) `2 = ((0. (TOP-REAL 2)) `2) - (qz `2) by TOPREAL3:3
.= - (qz `2) by JGRAPH_2:3 ;
((0. (TOP-REAL 2)) - qz) `1 = ((0. (TOP-REAL 2)) `1) - (qz `1) by TOPREAL3:3
.= - (qz `1) by JGRAPH_2:3 ;
then sqrt (((((0. (TOP-REAL 2)) - qz) `1) ^2) + ((((0. (TOP-REAL 2)) - qz) `2) ^2)) < r by A26, A36, A35, JGRAPH_2:3, XXREAL_0:2;
then |.((0. (TOP-REAL 2)) - qz).| < r by JGRAPH_1:30;
then dist (u0,pz) < r by JGRAPH_1:28;
hence z in W1 by METRIC_1:11; :: 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:63;
((q `1) / (q `2)) ^2 >= 0 by XREAL_1:63;
then 1 + (((q `1) / (q `2)) ^2) >= 1 + 0 by XREAL_1:7;
then A39: sqrt (1 + (((q `1) / (q `2)) ^2)) >= 1 by SQUARE_1:18, SQUARE_1:26;
then (sqrt (1 + (((q `1) / (q `2)) ^2))) ^2 >= sqrt (1 + (((q `1) / (q `2)) ^2)) by XREAL_1:151;
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:52
.= ((q `2) ^2) / ((sqrt (1 + (((q `1) / (q `2)) ^2))) ^2) by XCMPLX_1:76 ;
then A42: (qz `2) ^2 <= ((q `2) ^2) / 1 by A40, A38, XREAL_1:118;
A43: (q `1) ^2 >= 0 by XREAL_1:63;
(qz `1) ^2 = ((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))) ^2 by A25, A41, EUCLID:52
.= ((q `1) ^2) / ((sqrt (1 + (((q `1) / (q `2)) ^2))) ^2) by XCMPLX_1:76 ;
then (qz `1) ^2 <= ((q `1) ^2) / 1 by A40, A43, XREAL_1:118;
then A44: ((qz `1) ^2) + ((qz `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) by A42, XREAL_1:7;
( (qz `1) ^2 >= 0 & (qz `2) ^2 >= 0 ) by XREAL_1:63;
then A45: sqrt (((qz `1) ^2) + ((qz `2) ^2)) <= sqrt (((q `1) ^2) + ((q `2) ^2)) by A44, SQUARE_1:26;
A46: ((0. (TOP-REAL 2)) - qz) `2 = ((0. (TOP-REAL 2)) `2) - (qz `2) by TOPREAL3:3
.= - (qz `2) by JGRAPH_2:3 ;
((0. (TOP-REAL 2)) - qz) `1 = ((0. (TOP-REAL 2)) `1) - (qz `1) by TOPREAL3:3
.= - (qz `1) by JGRAPH_2:3 ;
then sqrt (((((0. (TOP-REAL 2)) - qz) `1) ^2) + ((((0. (TOP-REAL 2)) - qz) `2) ^2)) < r by A26, A46, A45, JGRAPH_2:3, XXREAL_0:2;
then |.((0. (TOP-REAL 2)) - qz).| < r by JGRAPH_1:30;
then dist (u0,pz) < r by JGRAPH_1:28;
hence z in W1 by METRIC_1:11; :: thesis: verum

end;

end;

end;

u0 in W1 by A19, GOBOARD6:1;
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 Th20;
then ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous ) by Th19;
hence ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = Sq_Circ & h is continuous ) by A15, A47, A1, A16, Th3; :: thesis: verum