reconsider f = Sq_Circ " as Function of (TOP-REAL 2),(TOP-REAL 2) by Th29;
reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:9;
A1: f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2) by Th28;
A2: 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))
A3: [#] ((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 A3, XBOOLE_0:def 5;
then A4: 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 A5: ( 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 A6: q `2 <> 0 ;
set q9 = |[((q `1) * (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) * (sqrt (1 + (((q `1) / (q `2)) ^2))))]|;
A7: |[((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;
A8: sqrt (1 + (((q `1) / (q `2)) ^2)) > 0 by Lm1, SQUARE_1:25;

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 * (q `2) = (q `2) * (sqrt (1 + (((q `1) / (q `2)) ^2))) by A7, EUCLID:52, EUCLID:54;
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))) ;
hence contradiction by A6, A8, XCMPLX_1:89; :: thesis: verum

end;

hence f . p <> f . (0. (TOP-REAL 2)) by A1, A5, Th28; :: 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 A4, 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;

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:89; :: thesis: verum

end;

hence f . p <> f . (0. (TOP-REAL 2)) by A1, A4, A9, Th28; :: thesis: verum

end;

end;

end;

A14: 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
A15: f . (0. (TOP-REAL 2)) in V and
A16: 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 A16, Lm16, PRE_TOPC:30;
then consider r being Real such that
A17: r > 0 and
A18: Ball (u0,r) c= V by A1, A15, TOPMETR:15;
reconsider r = r as Real ;
reconsider W1 = Ball (u0,r), V1 = Ball (u0,(r / (sqrt 2))) as Subset of (TOP-REAL 2) by EUCLID:67;
A19: f .: V1 c= W1

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f .: V1 or z in W1 )
A20: sqrt 2 > 0 by SQUARE_1:25;
assume z in f .: V1 ; :: thesis: z in W1
then consider y being object such that
A21: y in dom f and
A22: y in V1 and
A23: z = f . y by FUNCT_1:def 6;
z in rng f by A21, A23, 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 A21;
reconsider qy = q as Point of (Euclid 2) by EUCLID:67;
A24: (q `1) ^2 >= 0 by XREAL_1:63;
A25: (q `2) ^2 >= 0 by XREAL_1:63;
dist (u0,qy) < r / (sqrt 2) by A22, METRIC_1:11;
then |.((0. (TOP-REAL 2)) - q).| < r / (sqrt 2) by JGRAPH_1:28;
then sqrt (((((0. (TOP-REAL 2)) - q) `1) ^2) + ((((0. (TOP-REAL 2)) - q) `2) ^2)) < r / (sqrt 2) by JGRAPH_1:30;
then sqrt (((((0. (TOP-REAL 2)) `1) - (q `1)) ^2) + ((((0. (TOP-REAL 2)) - q) `2) ^2)) < r / (sqrt 2) by TOPREAL3:3;
then sqrt (((((0. (TOP-REAL 2)) `1) - (q `1)) ^2) + ((((0. (TOP-REAL 2)) `2) - (q `2)) ^2)) < r / (sqrt 2) by TOPREAL3:3;
then (sqrt (((q `1) ^2) + ((q `2) ^2))) * (sqrt 2) < (r / (sqrt 2)) * (sqrt 2) by A20, JGRAPH_2:3, XREAL_1:68;
then sqrt ((((q `1) ^2) + ((q `2) ^2)) * 2) < (r / (sqrt 2)) * (sqrt 2) by A24, A25, SQUARE_1:29;
then A26: sqrt ((((q `1) ^2) + ((q `2) ^2)) * 2) < r by A20, XCMPLX_1:87;

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

then z = 0. (TOP-REAL 2) by A23, Th28;
hence z in W1 by A17, GOBOARD6:1; :: 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: now :: thesis: not (q `1) ^2 <= 0

assume (q `1) ^2 <= 0 ; :: thesis: contradiction
then (q `1) ^2 = 0 by XREAL_1:63;
then A29: q `1 = 0 by XCMPLX_1:6;
then q `2 = 0 by A27;
hence contradiction by A27, A29, EUCLID:53, EUCLID:54; :: thesis: verum

end;

A30: (Sq_Circ ") . q = |[((q `1) * (sqrt (1 + (((q `2) / (q `1)) ^2)))),((q `2) * (sqrt (1 + (((q `2) / (q `1)) ^2))))]| by A27, Th28;
then qz `1 = (q `1) * (sqrt (1 + (((q `2) / (q `1)) ^2))) by A23, EUCLID:52;
then A31: (qz `1) ^2 = ((q `1) ^2) * ((sqrt (1 + (((q `2) / (q `1)) ^2))) ^2) ;
qz `2 = (q `2) * (sqrt (1 + (((q `2) / (q `1)) ^2))) by A23, A30, EUCLID:52;
then A32: (qz `2) ^2 = ((q `2) ^2) * ((sqrt (1 + (((q `2) / (q `1)) ^2))) ^2) ;
A33: 1 + (((q `2) / (q `1)) ^2) > 0 by Lm1;

now :: thesis: ( ( q `2 <= q `1 & - (q `1) <= q `2 & (q `2) ^2 <= (q `1) ^2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) & (q `2) ^2 <= (q `1) ^2 ) )

per cases ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) by A27;

case A34: ( q `2 <= q `1 & - (q `1) <= q `2 ) ; :: thesis: (q `2) ^2 <= (q `1) ^2

now :: thesis: ( ( 0 <= q `2 & (q `2) ^2 <= (q `1) ^2 ) or ( 0 > q `2 & (q `2) ^2 <= (q `1) ^2 ) )

per cases ( 0 <= q `2 or 0 > q `2 ) ;

case 0 <= q `2 ; :: thesis: (q `2) ^2 <= (q `1) ^2

hence (q `2) ^2 <= (q `1) ^2 by A34, SQUARE_1:15; :: thesis: verum

end;

case A35: 0 > q `2 ; :: thesis: (q `2) ^2 <= (q `1) ^2

- (- (q `1)) >= - (q `2) by A34, XREAL_1:24;
then (- (q `2)) ^2 <= (q `1) ^2 by A35, SQUARE_1:15;
hence (q `2) ^2 <= (q `1) ^2 ; :: thesis: verum

end;

end;

end;

hence (q `2) ^2 <= (q `1) ^2 ; :: thesis: verum

end;

case A36: ( q `2 >= q `1 & q `2 <= - (q `1) ) ; :: thesis: (q `2) ^2 <= (q `1) ^2

now :: thesis: ( ( 0 >= q `2 & (q `2) ^2 <= (q `1) ^2 ) or ( 0 < q `2 & (q `2) ^2 <= (q `1) ^2 ) )

per cases ( 0 >= q `2 or 0 < q `2 ) ;

case A37: 0 >= q `2 ; :: thesis: (q `2) ^2 <= (q `1) ^2

- (q `2) <= - (q `1) by A36, XREAL_1:24;
then (- (q `2)) ^2 <= (- (q `1)) ^2 by A37, SQUARE_1:15;
hence (q `2) ^2 <= (q `1) ^2 ; :: thesis: verum

end;

case 0 < q `2 ; :: thesis: (q `2) ^2 <= (q `1) ^2

then (q `2) ^2 <= (- (q `1)) ^2 by A36, SQUARE_1:15;
hence (q `2) ^2 <= (q `1) ^2 ; :: thesis: verum

end;

end;

end;

hence (q `2) ^2 <= (q `1) ^2 ; :: thesis: verum

end;

end;

end;

then ((q `2) ^2) / ((q `1) ^2) <= ((q `1) ^2) / ((q `1) ^2) by A28, XREAL_1:72;
then ((q `2) / (q `1)) ^2 <= ((q `1) ^2) / ((q `1) ^2) by XCMPLX_1:76;
then ((q `2) / (q `1)) ^2 <= 1 by A28, XCMPLX_1:60;
then A38: 1 + (((q `2) / (q `1)) ^2) <= 1 + 1 by XREAL_1:7;
then ((q `2) ^2) * (1 + (((q `2) / (q `1)) ^2)) <= ((q `2) ^2) * 2 by A25, XREAL_1:64;
then A39: (qz `2) ^2 <= ((q `2) ^2) * 2 by A33, A32, SQUARE_1:def 2;
((q `1) ^2) * (1 + (((q `2) / (q `1)) ^2)) <= ((q `1) ^2) * 2 by A24, A38, XREAL_1:64;
then (qz `1) ^2 <= ((q `1) ^2) * 2 by A33, A31, SQUARE_1:def 2;
then A40: ((qz `1) ^2) + ((qz `2) ^2) <= (((q `1) ^2) * 2) + (((q `2) ^2) * 2) by A39, XREAL_1:7;
( (qz `1) ^2 >= 0 & (qz `2) ^2 >= 0 ) by XREAL_1:63;
then A41: sqrt (((qz `1) ^2) + ((qz `2) ^2)) <= sqrt ((((q `1) ^2) * 2) + (((q `2) ^2) * 2)) by A40, SQUARE_1:26;
A42: ((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, A42, A41, 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 A43: ( 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

A44: now :: thesis: not (q `2) ^2 <= 0

assume (q `2) ^2 <= 0 ; :: thesis: contradiction
then (q `2) ^2 = 0 by XREAL_1:63;
then q `2 = 0 by XCMPLX_1:6;
hence contradiction by A43; :: thesis: verum

end;

now :: thesis: ( ( q `1 <= q `2 & - (q `2) <= q `1 & (q `1) ^2 <= (q `2) ^2 ) or ( q `1 >= q `2 & q `1 <= - (q `2) & (q `1) ^2 <= (q `2) ^2 ) )

per cases ( ( q `1 <= q `2 & - (q `2) <= q `1 ) or ( q `1 >= q `2 & q `1 <= - (q `2) ) ) by A43, JGRAPH_2:13;

case A45: ( q `1 <= q `2 & - (q `2) <= q `1 ) ; :: thesis: (q `1) ^2 <= (q `2) ^2

now :: thesis: ( ( 0 <= q `1 & (q `1) ^2 <= (q `2) ^2 ) or ( 0 > q `1 & (q `1) ^2 <= (q `2) ^2 ) )

per cases ( 0 <= q `1 or 0 > q `1 ) ;

case 0 <= q `1 ; :: thesis: (q `1) ^2 <= (q `2) ^2

hence (q `1) ^2 <= (q `2) ^2 by A45, SQUARE_1:15; :: thesis: verum

end;

case A46: 0 > q `1 ; :: thesis: (q `1) ^2 <= (q `2) ^2

- (- (q `2)) >= - (q `1) by A45, XREAL_1:24;
then (- (q `1)) ^2 <= (q `2) ^2 by A46, SQUARE_1:15;
hence (q `1) ^2 <= (q `2) ^2 ; :: thesis: verum

end;

end;

end;

hence (q `1) ^2 <= (q `2) ^2 ; :: thesis: verum

end;

case A47: ( q `1 >= q `2 & q `1 <= - (q `2) ) ; :: thesis: (q `1) ^2 <= (q `2) ^2

now :: thesis: ( ( 0 >= q `1 & (q `1) ^2 <= (q `2) ^2 ) or ( 0 < q `1 & (q `1) ^2 <= (q `2) ^2 ) )

per cases ( 0 >= q `1 or 0 < q `1 ) ;

case A48: 0 >= q `1 ; :: thesis: (q `1) ^2 <= (q `2) ^2

- (q `1) <= - (q `2) by A47, XREAL_1:24;
then (- (q `1)) ^2 <= (- (q `2)) ^2 by A48, SQUARE_1:15;
hence (q `1) ^2 <= (q `2) ^2 ; :: thesis: verum

end;

case 0 < q `1 ; :: thesis: (q `1) ^2 <= (q `2) ^2

then (q `1) ^2 <= (- (q `2)) ^2 by A47, SQUARE_1:15;
hence (q `1) ^2 <= (q `2) ^2 ; :: thesis: verum

end;

end;

end;

hence (q `1) ^2 <= (q `2) ^2 ; :: thesis: verum

end;

end;

end;

then ((q `1) ^2) / ((q `2) ^2) <= ((q `2) ^2) / ((q `2) ^2) by A44, XREAL_1:72;
then ((q `1) / (q `2)) ^2 <= ((q `2) ^2) / ((q `2) ^2) by XCMPLX_1:76;
then ((q `1) / (q `2)) ^2 <= 1 by A44, XCMPLX_1:60;
then A49: 1 + (((q `1) / (q `2)) ^2) <= 1 + 1 by XREAL_1:7;
then A50: ((q `2) ^2) * (1 + (((q `1) / (q `2)) ^2)) <= ((q `2) ^2) * 2 by A25, XREAL_1:64;
1 + (((q `1) / (q `2)) ^2) > 0 by Lm1;
then A51: (sqrt (1 + (((q `1) / (q `2)) ^2))) ^2 = 1 + (((q `1) / (q `2)) ^2) by SQUARE_1:def 2;
A52: ((q `1) ^2) * (1 + (((q `1) / (q `2)) ^2)) <= ((q `1) ^2) * 2 by A24, A49, XREAL_1:64;
A53: (Sq_Circ ") . q = |[((q `1) * (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) * (sqrt (1 + (((q `1) / (q `2)) ^2))))]| by A43, Th28;
then qz `1 = (q `1) * (sqrt (1 + (((q `1) / (q `2)) ^2))) by A23, EUCLID:52;
then A54: (qz `1) ^2 <= ((q `1) ^2) * 2 by A52, A51, SQUARE_1:9;
qz `2 = (q `2) * (sqrt (1 + (((q `1) / (q `2)) ^2))) by A23, A53, EUCLID:52;
then (qz `2) ^2 <= ((q `2) ^2) * 2 by A50, A51, SQUARE_1:9;
then A55: ((qz `2) ^2) + ((qz `1) ^2) <= (((q `2) ^2) * 2) + (((q `1) ^2) * 2) by A54, XREAL_1:7;
( (qz `2) ^2 >= 0 & (qz `1) ^2 >= 0 ) by XREAL_1:63;
then A56: sqrt (((qz `2) ^2) + ((qz `1) ^2)) <= sqrt ((((q `2) ^2) * 2) + (((q `1) ^2) * 2)) by A55, SQUARE_1:26;
A57: ((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) `2) ^2) + ((((0. (TOP-REAL 2)) - qz) `1) ^2)) < r by A26, A57, A56, 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;

A58: V1 is open by GOBOARD6:3;
sqrt 2 > 0 by SQUARE_1:25;
then u0 in V1 by A17, GOBOARD6:1, XREAL_1:139;
hence ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V ) by A18, A58, A19, XBOOLE_1:1; :: thesis: verum

end;

A59: 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 Th41;
hence ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = Sq_Circ " & h is continuous ) by A1, A59, A2, A14, Th3; :: thesis: verum