let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let C0, KXP, KXN, KYP, KYN be Subset of (TOP-REAL 2); :: thesis: for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let O, I be Point of I[01] ; :: thesis: ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 implies rng f meets rng g )
assume A1: ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 ) ; :: thesis: rng f meets rng g
reconsider ff = (Sq_Circ " ) * f as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:19, JGRAPH_3:39;
reconsider gg = (Sq_Circ " ) * g as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:19, JGRAPH_3:39;
consider h1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A2: ( h1 = Sq_Circ " & h1 is continuous ) by JGRAPH_3:52;
A3: dom ff = the carrier of I[01] by FUNCT_2:def 1;
A4: dom gg = the carrier of I[01] by FUNCT_2:def 1;
A5: dom f = the carrier of I[01] by FUNCT_2:def 1;
A6: dom g = the carrier of I[01] by FUNCT_2:def 1;
A7: ff is continuous by A1, A2;
A8: Sq_Circ " is one-to-one by JGRAPH_3:32;
then A9: ff is one-to-one by A1;
A10: gg is continuous by A1, A2;
A11: gg is one-to-one by A1, A8;
A12: ( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 )

proof

A13: ff . O = (Sq_Circ " ) . (f . O) by A3, FUNCT_1:22;
consider p1 being Point of (TOP-REAL 2) such that
A14: ( f . O = p1 & |.p1.| = 1 & p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) by A1;
A15: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) by A14, TOPRNS_1:24;
then A16: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by JGRAPH_3:38;
reconsider px = ff . O as Point of (TOP-REAL 2) ;
set q = px;
A17: ( px `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & px `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A13, A14, A16, EUCLID:56;
((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A18: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by SQUARE_1:93;

A19: now

assume A20: ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then A21: p1 `1 = 0 by A17, A18, XCMPLX_1:6;
p1 `2 = 0 by A17, A18, A20, XCMPLX_1:6;
hence contradiction by A15, A21, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) ) by A14, A18, XREAL_1:66;
then A22: ( ( p1 `2 <= p1 `1 & (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A17, A18, XREAL_1:66;
then A23: ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A17, A18, XREAL_1:66;
A24: p1 = Sq_Circ . px by A13, A14, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A25: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A19, A23, JGRAPH_2:11, JGRAPH_3:def 1;
A26: ( |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `1 = (px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) & |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `2 = (px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ) by EUCLID:56;
((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
then A27: 1 + (((px `2 ) / (px `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A28: sqrt (1 + (((px `2 ) / (px `1 )) ^2 )) > 0 by SQUARE_1:93;
A29: px `1 <> 0 by A17, A18, A19, A22, XREAL_1:66;

now

|.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A24, A25, A26, JGRAPH_3:10
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by A27, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A27, SQUARE_1:def 4
.= (((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 )) by XCMPLX_1:63 ;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 ))) * (1 + (((px `2 ) / (px `1 )) ^2 )) = 1 * (1 + (((px `2 ) / (px `1 )) ^2 )) by A14;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) = 1 + (((px `2 ) / (px `1 )) ^2 ) by A27, XCMPLX_1:88;
then (((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1 = ((px `2 ) ^2 ) / ((px `1 ) ^2 ) by XCMPLX_1:77;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1) * ((px `1 ) ^2 ) = (px `2 ) ^2 by A29, XCMPLX_1:6, XCMPLX_1:88;
hence ((((px `1 ) ^2 ) - 1) * ((px `1 ) ^2 )) + ((((px `1 ) ^2 ) - 1) * ((px `2 ) ^2 )) = 0 ; :: thesis: verum

end;

then A30: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) = 0 ;
((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A19, COMPLEX1:2;
then ((px `1 ) - 1) * ((px `1 ) + 1) = 0 by A30, XCMPLX_1:6;
then A31: ( (px `1 ) - 1 = 0 or (px `1 ) + 1 = 0 ) by XCMPLX_1:6;

A32: now

assume A33: px `1 = 1 ; :: thesis: contradiction
- (p1 `2 ) >= - (- (p1 `1 )) by A14, XREAL_1:26;
then - (p1 `2 ) > 0 by A24, A25, A26, A28, A33, XREAL_1:141;
then - (- (p1 `2 )) < - 0 ;
hence contradiction by A14, A24, A25, A26, A28, A33; :: thesis: verum

end;

A34: ff . I = (Sq_Circ " ) . (f . I) by A3, FUNCT_1:22;
consider p2 being Point of (TOP-REAL 2) such that
A35: ( f . I = p2 & |.p2.| = 1 & p2 `2 <= p2 `1 & p2 `2 >= - (p2 `1 ) ) by A1;
A36: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) by A35, TOPRNS_1:24;
then A37: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by JGRAPH_3:38;
reconsider py = ff . I as Point of (TOP-REAL 2) ;
A38: ( py `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & py `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) by A34, A35, A37, EUCLID:56;
((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A39: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;

A40: now

assume A41: ( py `1 = 0 & py `2 = 0 ) ; :: thesis: contradiction
then A42: p2 `1 = 0 by A38, A39, XCMPLX_1:6;
p2 `2 = 0 by A38, A39, A41, XCMPLX_1:6;
hence contradiction by A36, A42, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A43: now

( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( py `2 >= py `1 & py `2 <= - (py `1 ) ) ) by A35, A39, XREAL_1:66;
hence ( ( (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & - (py `1 ) <= py `2 ) or ( py `2 >= py `1 & py `2 <= - (py `1 ) ) ) by A38, A39, XREAL_1:66; :: thesis: verum

end;

A44: p2 = Sq_Circ . py by A34, A35, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A45: Sq_Circ . py = |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| by A38, A40, A43, JGRAPH_2:11, JGRAPH_3:def 1;
A46: ( |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 = (py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) & |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 = (py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ) by EUCLID:56;
((py `2 ) / (py `1 )) ^2 >= 0 by XREAL_1:65;
then A47: 1 + (((py `2 ) / (py `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A48: sqrt (1 + (((py `2 ) / (py `1 )) ^2 )) > 0 by SQUARE_1:93;
A49: py `1 <> 0 by A38, A40, A43;

now

|.p2.| ^2 = (((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) + (((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) by A44, A45, A46, JGRAPH_3:10
.= (((py `1 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) + (((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((py `1 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) + (((py `2 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((py `1 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) + (((py `2 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) by A47, SQUARE_1:def 4
.= (((py `1 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) + (((py `2 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) by A47, SQUARE_1:def 4
.= (((py `1 ) ^2 ) + ((py `2 ) ^2 )) / (1 + (((py `2 ) / (py `1 )) ^2 )) by XCMPLX_1:63 ;
then ((((py `1 ) ^2 ) + ((py `2 ) ^2 )) / (1 + (((py `2 ) / (py `1 )) ^2 ))) * (1 + (((py `2 ) / (py `1 )) ^2 )) = 1 * (1 + (((py `2 ) / (py `1 )) ^2 )) by A35;
then ((py `1 ) ^2 ) + ((py `2 ) ^2 ) = 1 + (((py `2 ) / (py `1 )) ^2 ) by A47, XCMPLX_1:88;
then (((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1 = ((py `2 ) ^2 ) / ((py `1 ) ^2 ) by XCMPLX_1:77;
then ((((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1) * ((py `1 ) ^2 ) = (py `2 ) ^2 by A49, XCMPLX_1:6, XCMPLX_1:88;
hence ((((py `1 ) ^2 ) - 1) * ((py `1 ) ^2 )) + ((((py `1 ) ^2 ) - 1) * ((py `2 ) ^2 )) = 0 ; :: thesis: verum

end;

then A50: (((py `1 ) ^2 ) - 1) * (((py `1 ) ^2 ) + ((py `2 ) ^2 )) = 0 ;
((py `1 ) ^2 ) + ((py `2 ) ^2 ) <> 0 by A40, COMPLEX1:2;
then ((py `1 ) - 1) * ((py `1 ) + 1) = 0 by A50, XCMPLX_1:6;
then A51: ( (py `1 ) - 1 = 0 or (py `1 ) + 1 = 0 ) by XCMPLX_1:6;

A52: now

assume A53: py `1 = - 1 ; :: thesis: contradiction
- (p2 `2 ) <= - (- (p2 `1 )) by A35, XREAL_1:26;
then - (p2 `2 ) < 0 by A44, A45, A46, A48, A53, XREAL_1:143;
then - (- (p2 `2 )) > - 0 ;
hence contradiction by A35, A44, A45, A46, A48, A53; :: thesis: verum

end;

A54: gg . O = (Sq_Circ " ) . (g . O) by A4, FUNCT_1:22;
consider p3 being Point of (TOP-REAL 2) such that
A55: ( g . O = p3 & |.p3.| = 1 & p3 `2 <= p3 `1 & p3 `2 <= - (p3 `1 ) ) by A1;
A56: - (p3 `2 ) >= - (- (p3 `1 )) by A55, XREAL_1:26;
then A57: ( p3 <> 0. (TOP-REAL 2) & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) ) by A55, TOPRNS_1:24;
then A58: (Sq_Circ " ) . p3 = |[((p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by JGRAPH_3:40;
reconsider pz = gg . O as Point of (TOP-REAL 2) ;
A59: ( pz `2 = (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) & pz `1 = (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) by A54, A55, A58, EUCLID:56;
((p3 `1 ) / (p3 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p3 `1 ) / (p3 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A60: sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )) > 0 by SQUARE_1:93;

A61: now

assume A62: ( pz `2 = 0 & pz `1 = 0 ) ; :: thesis: contradiction
then A63: p3 `2 = 0 by A59, A60, XCMPLX_1:6;
p3 `1 = 0 by A59, A60, A62, XCMPLX_1:6;
hence contradiction by A57, A63, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A64: now

( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (- (p3 `2 )) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) ) by A55, A56, A60, XREAL_1:66;
then ( ( p3 `1 <= p3 `2 & (- (p3 `2 )) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A59, A60, XREAL_1:66;
hence ( ( (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) & - (pz `2 ) <= pz `1 ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A59, A60, XREAL_1:66; :: thesis: verum

end;

A65: p3 = Sq_Circ . pz by A54, A55, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A66: Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A59, A61, A64, JGRAPH_2:11, JGRAPH_3:14;
A67: ( |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `2 = (pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) & |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `1 = (pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ) by EUCLID:56;
((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
then A68: 1 + (((pz `1 ) / (pz `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A69: sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )) > 0 by SQUARE_1:93;
A70: pz `2 <> 0 by A59, A61, A64;
A71: |.p3.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A65, A66, A67, JGRAPH_3:10
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by A68, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A68, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;

now

((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) * (1 + (((pz `1 ) / (pz `2 )) ^2 )) = 1 * (1 + (((pz `1 ) / (pz `2 )) ^2 )) by A55, A71;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) = 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A68, XCMPLX_1:88;
then (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1 = ((pz `1 ) ^2 ) / ((pz `2 ) ^2 ) by XCMPLX_1:77;
then ((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1) * ((pz `2 ) ^2 ) = (pz `1 ) ^2 by A70, XCMPLX_1:6, XCMPLX_1:88;
hence ((((pz `2 ) ^2 ) * (((pz `2 ) ^2 ) - 1)) + (((pz `2 ) ^2 ) * ((pz `1 ) ^2 ))) - (1 * ((pz `1 ) ^2 )) = 0 ; :: thesis: verum

end;

then A72: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) = 0 ;
((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A61, COMPLEX1:2;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) = 0 by A72, XCMPLX_1:6;
then A73: ( (pz `2 ) - 1 = 0 or (pz `2 ) + 1 = 0 ) by XCMPLX_1:6;

A74: now

assume A75: pz `2 = 1 ; :: thesis: contradiction
then - (p3 `1 ) > 0 by A55, A65, A66, A67, A69, XREAL_1:141;
then - (- (p3 `1 )) < - 0 ;
hence contradiction by A55, A65, A66, A67, A69, A75; :: thesis: verum

end;

A76: gg . I = (Sq_Circ " ) . (g . I) by A4, FUNCT_1:22;
consider p4 being Point of (TOP-REAL 2) such that
A77: ( g . I = p4 & |.p4.| = 1 & p4 `2 >= p4 `1 & p4 `2 >= - (p4 `1 ) ) by A1;
A78: - (p4 `2 ) <= - (- (p4 `1 )) by A77, XREAL_1:26;
then A79: ( p4 <> 0. (TOP-REAL 2) & ( ( p4 `1 <= p4 `2 & - (p4 `2 ) <= p4 `1 ) or ( p4 `1 >= p4 `2 & p4 `1 <= - (p4 `2 ) ) ) ) by A77, TOPRNS_1:24;
then A80: (Sq_Circ " ) . p4 = |[((p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )))),((p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))))]| by JGRAPH_3:40;
reconsider pu = gg . I as Point of (TOP-REAL 2) ;
A81: ( pu `2 = (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) & pu `1 = (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) ) by A76, A77, A80, EUCLID:56;
((p4 `1 ) / (p4 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p4 `1 ) / (p4 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A82: sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )) > 0 by SQUARE_1:93;

A83: now

assume A84: ( pu `2 = 0 & pu `1 = 0 ) ; :: thesis: contradiction
then A85: p4 `2 = 0 by A81, A82, XCMPLX_1:6;
p4 `1 = 0 by A81, A82, A84, XCMPLX_1:6;
hence contradiction by A79, A85, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A86: now

( ( p4 `1 <= p4 `2 & (- (p4 `2 )) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) <= (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) ) or ( pu `1 >= pu `2 & pu `1 <= - (pu `2 ) ) ) by A77, A78, A82, XREAL_1:66;
hence ( ( (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) <= (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) & - (pu `2 ) <= pu `1 ) or ( pu `1 >= pu `2 & pu `1 <= - (pu `2 ) ) ) by A81, A82, XREAL_1:66; :: thesis: verum

end;

A87: p4 = Sq_Circ . pu by A76, A77, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A88: Sq_Circ . pu = |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| by A81, A83, A86, JGRAPH_2:11, JGRAPH_3:14;
A89: ( |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| `2 = (pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) & |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| `1 = (pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ) by EUCLID:56;
((pu `1 ) / (pu `2 )) ^2 >= 0 by XREAL_1:65;
then A90: 1 + (((pu `1 ) / (pu `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A91: sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )) > 0 by SQUARE_1:93;
A92: pu `2 <> 0 by A81, A83, A86;

now

|.p4.| ^2 = (((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) + (((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) by A87, A88, A89, JGRAPH_3:10
.= (((pu `2 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) + (((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((pu `2 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) + (((pu `1 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((pu `2 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) + (((pu `1 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) by A90, SQUARE_1:def 4
.= (((pu `2 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) + (((pu `1 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) by A90, SQUARE_1:def 4
.= (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) / (1 + (((pu `1 ) / (pu `2 )) ^2 )) by XCMPLX_1:63 ;
then ((((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) * (1 + (((pu `1 ) / (pu `2 )) ^2 )) = 1 * (1 + (((pu `1 ) / (pu `2 )) ^2 )) by A77;
then ((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) = 1 + (((pu `1 ) / (pu `2 )) ^2 ) by A90, XCMPLX_1:88;
then (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1 = ((pu `1 ) ^2 ) / ((pu `2 ) ^2 ) by XCMPLX_1:77;
then ((((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1) * ((pu `2 ) ^2 ) = (pu `1 ) ^2 by A92, XCMPLX_1:6, XCMPLX_1:88;
hence ((((pu `2 ) ^2 ) - 1) * ((pu `2 ) ^2 )) + ((((pu `2 ) ^2 ) - 1) * ((pu `1 ) ^2 )) = 0 ; :: thesis: verum

end;

then A93: (((pu `2 ) ^2 ) - 1) * (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) = 0 ;
((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) <> 0 by A83, COMPLEX1:2;
then ((pu `2 ) - 1) * ((pu `2 ) + 1) = 0 by A93, XCMPLX_1:6;
then A94: ( (pu `2 ) - 1 = 0 or (pu `2 ) + 1 = 0 ) by XCMPLX_1:6;

now

assume A95: pu `2 = - 1 ; :: thesis: contradiction
then - (p4 `1 ) < 0 by A77, A87, A88, A89, A91, XREAL_1:143;
then - (- (p4 `1 )) > - 0 ;
hence contradiction by A77, A87, A88, A89, A91, A95; :: thesis: verum

end;

hence ( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 ) by A31, A32, A51, A52, A73, A74, A94; :: thesis: verum

end;

A96: for r being Point of I[01] holds
( ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) & ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) )

proof

let r be Point of I[01] ; :: thesis: ( ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) & ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) )
A97: ff . r = (Sq_Circ " ) . (f . r) by A3, FUNCT_1:22;
f . r in rng f by A5, FUNCT_1:12;
then f . r in C0 by A1;
then consider p1 being Point of (TOP-REAL 2) such that
A98: ( f . r = p1 & |.p1.| >= 1 ) by A1;

A99: now

per cases ( p1 = 0. (TOP-REAL 2) or ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) or ( p1 <> 0. (TOP-REAL 2) & not ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) & not ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) ;

case p1 = 0. (TOP-REAL 2) ; :: thesis: contradiction

hence contradiction by A98, TOPRNS_1:24; :: thesis: verum

end;

case A100: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) ; :: thesis: ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 )

then A101: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by JGRAPH_3:38;
reconsider px = ff . r as Point of (TOP-REAL 2) ;
set q = px;
A102: ( px `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & px `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A97, A98, A101, EUCLID:56;
((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A103: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by SQUARE_1:93;

A104: now

assume A105: ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then A106: p1 `1 = 0 by A102, A103, XCMPLX_1:6;
p1 `2 = 0 by A102, A103, A105, XCMPLX_1:6;
hence contradiction by A100, A106, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A107: now

( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) ) by A100, A103, XREAL_1:66;
then ( ( p1 `2 <= p1 `1 & (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A102, A103, XREAL_1:66;
hence ( ( (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A102, A103, XREAL_1:66; :: thesis: verum

end;

A108: p1 = Sq_Circ . px by A97, A98, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A109: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A102, A104, A107, JGRAPH_2:11, JGRAPH_3:def 1;
A110: ( |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `1 = (px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) & |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `2 = (px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ) by EUCLID:56;
A111: (px `1 ) ^2 >= 0 by XREAL_1:65;
((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
then A112: 1 + (((px `2 ) / (px `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
|.p1.| ^2 >= |.p1.| by A98, XREAL_1:153;
then A113: |.p1.| ^2 >= 1 by A98, XXREAL_0:2;
A114: px `1 <> 0 by A102, A104, A107;

now

|.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A108, A109, A110, JGRAPH_3:10
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by A112, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A112, SQUARE_1:def 4
.= (((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 )) by XCMPLX_1:63 ;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 ))) * (1 + (((px `2 ) / (px `1 )) ^2 )) >= 1 * (1 + (((px `2 ) / (px `1 )) ^2 )) by A112, A113, XREAL_1:66;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 1 + (((px `2 ) / (px `1 )) ^2 ) by A112, XCMPLX_1:88;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 1 + (((px `2 ) ^2 ) / ((px `1 ) ^2 )) by XCMPLX_1:77;
then (((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1 >= (1 + (((px `2 ) ^2 ) / ((px `1 ) ^2 ))) - 1 by XREAL_1:11;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1) * ((px `1 ) ^2 ) >= (((px `2 ) ^2 ) / ((px `1 ) ^2 )) * ((px `1 ) ^2 ) by A111, XREAL_1:66;
then (((px `1 ) ^2 ) + (((px `2 ) ^2 ) - 1)) * ((px `1 ) ^2 ) >= (px `2 ) ^2 by A114, XCMPLX_1:6, XCMPLX_1:88;
then ((((px `1 ) ^2 ) * ((px `1 ) ^2 )) + (((px `1 ) ^2 ) * (((px `2 ) ^2 ) - 1))) - ((px `2 ) ^2 ) >= ((px `2 ) ^2 ) - ((px `2 ) ^2 ) by XREAL_1:11;
hence ((((px `1 ) ^2 ) - 1) * ((px `1 ) ^2 )) + ((((px `1 ) ^2 ) - 1) * ((px `2 ) ^2 )) >= 0 ; :: thesis: verum

end;

then A115: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) >= 0 ;
A116: ((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A104, COMPLEX1:2;
(px `2 ) ^2 >= 0 by XREAL_1:65;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 0 + 0 by A111;
then ((px `1 ) - 1) * ((px `1 ) + 1) >= 0 by A115, A116, XREAL_1:134;
hence ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) by XREAL_1:97; :: thesis: verum

end;

case A117: ( p1 <> 0. (TOP-REAL 2) & not ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) & not ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ; :: thesis: ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 )

then A118: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| by JGRAPH_3:38;
A119: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2 ) ) ) ) by A117, JGRAPH_2:23;
reconsider pz = ff . r as Point of (TOP-REAL 2) ;
A120: ( pz `2 = (p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) & pz `1 = (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) by A97, A98, A118, EUCLID:56;
((p1 `1 ) / (p1 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `1 ) / (p1 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A121: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) > 0 by SQUARE_1:93;

A122: now

assume ( pz `2 = 0 & pz `1 = 0 ) ; :: thesis: contradiction
then p1 `2 = 0 by A120, A121, XCMPLX_1:6;
hence contradiction by A117; :: thesis: verum

end;

A124: now

( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) <= (- (p1 `2 )) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) ) by A119, A121, XREAL_1:66;
then ( ( p1 `1 <= p1 `2 & (- (p1 `2 )) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) <= (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A120, A121, XREAL_1:66;
hence ( ( (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) & - (pz `2 ) <= pz `1 ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A120, A121, XREAL_1:66; :: thesis: verum

end;

A125: p1 = Sq_Circ . pz by A97, A98, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A126: Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A120, A122, A124, JGRAPH_2:11, JGRAPH_3:14;
A127: ( |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `2 = (pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) & |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `1 = (pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ) by EUCLID:56;
A128: (pz `2 ) ^2 >= 0 by XREAL_1:65;
((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
then A129: 1 + (((pz `1 ) / (pz `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
|.p1.| ^2 >= |.p1.| by A98, XREAL_1:153;
then A130: |.p1.| ^2 >= 1 by A98, XXREAL_0:2;
A131: pz `2 <> 0 by A120, A122, A124;
A132: |.p1.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A125, A126, A127, JGRAPH_3:10
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by A129, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A129, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;

now

((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) * (1 + (((pz `1 ) / (pz `2 )) ^2 )) >= 1 * (1 + (((pz `1 ) / (pz `2 )) ^2 )) by A129, A130, A132, XREAL_1:66;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A129, XCMPLX_1:88;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 1 + (((pz `1 ) ^2 ) / ((pz `2 ) ^2 )) by XCMPLX_1:77;
then (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1 >= (1 + (((pz `1 ) ^2 ) / ((pz `2 ) ^2 ))) - 1 by XREAL_1:11;
then ((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1) * ((pz `2 ) ^2 ) >= (((pz `1 ) ^2 ) / ((pz `2 ) ^2 )) * ((pz `2 ) ^2 ) by A128, XREAL_1:66;
then (((pz `2 ) ^2 ) + (((pz `1 ) ^2 ) - 1)) * ((pz `2 ) ^2 ) >= (pz `1 ) ^2 by A131, XCMPLX_1:6, XCMPLX_1:88;
then ((((pz `2 ) ^2 ) * ((pz `2 ) ^2 )) + (((pz `2 ) ^2 ) * (((pz `1 ) ^2 ) - 1))) - ((pz `1 ) ^2 ) >= ((pz `1 ) ^2 ) - ((pz `1 ) ^2 ) by XREAL_1:11;
hence ((((pz `2 ) ^2 ) * (((pz `2 ) ^2 ) - 1)) + (((pz `2 ) ^2 ) * ((pz `1 ) ^2 ))) - (1 * ((pz `1 ) ^2 )) >= 0 ; :: thesis: verum

end;

then A133: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) >= 0 ;
A134: ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A122, COMPLEX1:2;
(pz `1 ) ^2 >= 0 by XREAL_1:65;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 0 + 0 by A128;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) >= 0 by A133, A134, XREAL_1:134;
hence ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) by XREAL_1:97; :: thesis: verum

end;

end;

end;

A135: gg . r = (Sq_Circ " ) . (g . r) by A4, FUNCT_1:22;
g . r in rng g by A6, FUNCT_1:12;
then g . r in C0 by A1;
then consider p2 being Point of (TOP-REAL 2) such that
A136: ( g . r = p2 & |.p2.| >= 1 ) by A1;

now

per cases ( p2 = 0. (TOP-REAL 2) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ;

case p2 = 0. (TOP-REAL 2) ; :: thesis: contradiction

hence contradiction by A136, TOPRNS_1:24; :: thesis: verum

end;

case A137: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 )

then A138: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by JGRAPH_3:38;
reconsider px = gg . r as Point of (TOP-REAL 2) ;
set q = px;
A139: (Sq_Circ " ) . p2 = px by A4, A136, FUNCT_1:22;
A140: ( px `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & px `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) by A135, A136, A138, EUCLID:56;
((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A141: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;

A142: now

assume A143: ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then A144: p2 `1 = 0 by A140, A141, XCMPLX_1:6;
p2 `2 = 0 by A140, A141, A143, XCMPLX_1:6;
hence contradiction by A137, A144, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A145: now

( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) ) by A137, A141, XREAL_1:66;
then ( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A140, A141, XREAL_1:66;
hence ( ( (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A140, A141, XREAL_1:66; :: thesis: verum

end;

A146: p2 = Sq_Circ . px by A139, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A147: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A140, A142, A145, JGRAPH_2:11, JGRAPH_3:def 1;
A148: ( |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `1 = (px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) & |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `2 = (px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ) by EUCLID:56;
A149: (px `1 ) ^2 >= 0 by XREAL_1:65;
((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
then A150: 1 + (((px `2 ) / (px `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
|.p2.| ^2 >= |.p2.| by A136, XREAL_1:153;
then A151: |.p2.| ^2 >= 1 by A136, XXREAL_0:2;
A152: px `1 <> 0 by A140, A142, A145;

now

|.p2.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A146, A147, A148, JGRAPH_3:10
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by A150, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A150, SQUARE_1:def 4
.= (((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 )) by XCMPLX_1:63 ;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 ))) * (1 + (((px `2 ) / (px `1 )) ^2 )) >= 1 * (1 + (((px `2 ) / (px `1 )) ^2 )) by A150, A151, XREAL_1:66;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 1 + (((px `2 ) / (px `1 )) ^2 ) by A150, XCMPLX_1:88;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 1 + (((px `2 ) ^2 ) / ((px `1 ) ^2 )) by XCMPLX_1:77;
then (((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1 >= (1 + (((px `2 ) ^2 ) / ((px `1 ) ^2 ))) - 1 by XREAL_1:11;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1) * ((px `1 ) ^2 ) >= (((px `2 ) ^2 ) / ((px `1 ) ^2 )) * ((px `1 ) ^2 ) by A149, XREAL_1:66;
then (((px `1 ) ^2 ) + (((px `2 ) ^2 ) - 1)) * ((px `1 ) ^2 ) >= (px `2 ) ^2 by A152, XCMPLX_1:6, XCMPLX_1:88;
then ((((px `1 ) ^2 ) * ((px `1 ) ^2 )) + (((px `1 ) ^2 ) * (((px `2 ) ^2 ) - 1))) - ((px `2 ) ^2 ) >= ((px `2 ) ^2 ) - ((px `2 ) ^2 ) by XREAL_1:11;
hence ((((px `1 ) ^2 ) - 1) * ((px `1 ) ^2 )) + ((((px `1 ) ^2 ) - 1) * ((px `2 ) ^2 )) >= 0 ; :: thesis: verum

end;

then A153: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) >= 0 ;
A154: ((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A142, COMPLEX1:2;
(px `2 ) ^2 >= 0 by XREAL_1:65;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 0 + 0 by A149;
then ((px `1 ) - 1) * ((px `1 ) + 1) >= 0 by A153, A154, XREAL_1:134;
hence ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) by XREAL_1:97; :: thesis: verum

end;

case A155: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 )

then A156: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by JGRAPH_3:38;
A157: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) ) by A155, JGRAPH_2:23;
reconsider pz = gg . r as Point of (TOP-REAL 2) ;
A158: ( pz `2 = (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) & pz `1 = (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) by A135, A136, A156, EUCLID:56;
((p2 `1 ) / (p2 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A159: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by SQUARE_1:93;

A160: now

assume ( pz `2 = 0 & pz `1 = 0 ) ; :: thesis: contradiction
then p2 `2 = 0 by A158, A159, XCMPLX_1:6;
hence contradiction by A155; :: thesis: verum

end;

A162: now

( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (- (p2 `2 )) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) ) by A157, A159, XREAL_1:66;
then ( ( p2 `1 <= p2 `2 & (- (p2 `2 )) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A158, A159, XREAL_1:66;
hence ( ( (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) & - (pz `2 ) <= pz `1 ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A158, A159, XREAL_1:66; :: thesis: verum

end;

A163: p2 = Sq_Circ . pz by A135, A136, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A164: Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A158, A160, A162, JGRAPH_2:11, JGRAPH_3:14;
A165: ( |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `2 = (pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) & |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `1 = (pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ) by EUCLID:56;
A166: (pz `2 ) ^2 >= 0 by XREAL_1:65;
((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
then A167: 1 + (((pz `1 ) / (pz `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
|.p2.| ^2 >= |.p2.| by A136, XREAL_1:153;
then A168: |.p2.| ^2 >= 1 by A136, XXREAL_0:2;
A169: pz `2 <> 0 by A158, A160, A162;
A170: |.p2.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A163, A164, A165, JGRAPH_3:10
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by A167, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A167, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;

now

((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) * (1 + (((pz `1 ) / (pz `2 )) ^2 )) >= 1 * (1 + (((pz `1 ) / (pz `2 )) ^2 )) by A167, A168, A170, XREAL_1:66;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A167, XCMPLX_1:88;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 1 + (((pz `1 ) ^2 ) / ((pz `2 ) ^2 )) by XCMPLX_1:77;
then (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1 >= (1 + (((pz `1 ) ^2 ) / ((pz `2 ) ^2 ))) - 1 by XREAL_1:11;
then ((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1) * ((pz `2 ) ^2 ) >= (((pz `1 ) ^2 ) / ((pz `2 ) ^2 )) * ((pz `2 ) ^2 ) by A166, XREAL_1:66;
then (((pz `2 ) ^2 ) + (((pz `1 ) ^2 ) - 1)) * ((pz `2 ) ^2 ) >= (pz `1 ) ^2 by A169, XCMPLX_1:6, XCMPLX_1:88;
then ((((pz `2 ) ^2 ) * ((pz `2 ) ^2 )) + (((pz `2 ) ^2 ) * (((pz `1 ) ^2 ) - 1))) - ((pz `1 ) ^2 ) >= ((pz `1 ) ^2 ) - ((pz `1 ) ^2 ) by XREAL_1:11;
hence ((((pz `2 ) ^2 ) * (((pz `2 ) ^2 ) - 1)) + (((pz `2 ) ^2 ) * ((pz `1 ) ^2 ))) - (1 * ((pz `1 ) ^2 )) >= 0 ; :: thesis: verum

end;

then A171: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) >= 0 ;
A172: ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A160, COMPLEX1:2;
(pz `1 ) ^2 >= 0 by XREAL_1:65;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 0 + 0 by A166;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) >= 0 by A171, A172, XREAL_1:134;
hence ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) by XREAL_1:97; :: thesis: verum

end;

end;

end;

hence ( ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) & ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) ) by A99; :: thesis: verum

end;

( - 1 <= (ff . O) `2 & (ff . O) `2 <= 1 & - 1 <= (ff . I) `2 & (ff . I) `2 <= 1 & - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 & - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )

proof

A173: ff . O = (Sq_Circ " ) . (f . O) by A3, FUNCT_1:22;
consider p1 being Point of (TOP-REAL 2) such that
A174: ( f . O = p1 & |.p1.| = 1 & p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) by A1;
A175: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) by A174, TOPRNS_1:24;
then A176: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by JGRAPH_3:38;
reconsider px = ff . O as Point of (TOP-REAL 2) ;
set q = px;
A177: ( px `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & px `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A173, A174, A176, EUCLID:56;
((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A178: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by SQUARE_1:93;

A179: now

assume A180: ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then A181: p1 `1 = 0 by A177, A178, XCMPLX_1:6;
p1 `2 = 0 by A177, A178, A180, XCMPLX_1:6;
hence contradiction by A175, A181, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) ) by A174, A178, XREAL_1:66;
then A182: ( ( p1 `2 <= p1 `1 & (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A177, A178, XREAL_1:66;
then A183: ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A177, A178, XREAL_1:66;
A184: p1 = Sq_Circ . px by A173, A174, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A185: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A179, A183, JGRAPH_2:11, JGRAPH_3:def 1;
A186: ( |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `1 = (px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) & |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| `2 = (px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ) by EUCLID:56;
((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
then A187: 1 + (((px `2 ) / (px `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
A188: px `1 <> 0 by A177, A178, A179, A182, XREAL_1:66;

now

|.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A184, A185, A186, JGRAPH_3:10
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by A187, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A187, SQUARE_1:def 4
.= (((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 )) by XCMPLX_1:63 ;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 ))) * (1 + (((px `2 ) / (px `1 )) ^2 )) = 1 * (1 + (((px `2 ) / (px `1 )) ^2 )) by A174;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) = 1 + (((px `2 ) / (px `1 )) ^2 ) by A187, XCMPLX_1:88;
then (((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1 = ((px `2 ) ^2 ) / ((px `1 ) ^2 ) by XCMPLX_1:77;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1) * ((px `1 ) ^2 ) = (px `2 ) ^2 by A188, XCMPLX_1:6, XCMPLX_1:88;
hence ((((px `1 ) ^2 ) - 1) * ((px `1 ) ^2 )) + ((((px `1 ) ^2 ) - 1) * ((px `2 ) ^2 )) = 0 ; :: thesis: verum

end;

then A189: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) = 0 ;
((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A179, COMPLEX1:2;
then ((px `1 ) - 1) * ((px `1 ) + 1) = 0 by A189, XCMPLX_1:6;
then ( (px `1 ) - 1 = 0 or (px `1 ) + 1 = 0 ) by XCMPLX_1:6;
then A190: ( px `1 = 1 or px `1 = 0 - 1 ) ;
A191: ff . I = (Sq_Circ " ) . (f . I) by A3, FUNCT_1:22;
consider p2 being Point of (TOP-REAL 2) such that
A192: ( f . I = p2 & |.p2.| = 1 & p2 `2 <= p2 `1 & p2 `2 >= - (p2 `1 ) ) by A1;
A193: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) by A192, TOPRNS_1:24;
then A194: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by JGRAPH_3:38;
reconsider py = ff . I as Point of (TOP-REAL 2) ;
A195: ( py `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & py `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) by A191, A192, A194, EUCLID:56;
((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A196: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;

A197: now

assume A198: ( py `1 = 0 & py `2 = 0 ) ; :: thesis: contradiction
then A199: p2 `1 = 0 by A195, A196, XCMPLX_1:6;
p2 `2 = 0 by A195, A196, A198, XCMPLX_1:6;
hence contradiction by A193, A199, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A200: now

( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( py `2 >= py `1 & py `2 <= - (py `1 ) ) ) by A192, A196, XREAL_1:66;
hence ( ( (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & - (py `1 ) <= py `2 ) or ( py `2 >= py `1 & py `2 <= - (py `1 ) ) ) by A195, A196, XREAL_1:66; :: thesis: verum

end;

A201: p2 = Sq_Circ . py by A191, A192, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A202: Sq_Circ . py = |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| by A195, A197, A200, JGRAPH_2:11, JGRAPH_3:def 1;
A203: ( |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 = (py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) & |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 = (py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ) by EUCLID:56;
((py `2 ) / (py `1 )) ^2 >= 0 by XREAL_1:65;
then A204: 1 + (((py `2 ) / (py `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
A205: py `1 <> 0 by A195, A197, A200;

now

|.p2.| ^2 = (((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) + (((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) by A201, A202, A203, JGRAPH_3:10
.= (((py `1 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) + (((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((py `1 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) + (((py `2 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((py `1 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) + (((py `2 ) ^2 ) / ((sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ^2 )) by A204, SQUARE_1:def 4
.= (((py `1 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) + (((py `2 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) by A204, SQUARE_1:def 4
.= (((py `1 ) ^2 ) + ((py `2 ) ^2 )) / (1 + (((py `2 ) / (py `1 )) ^2 )) by XCMPLX_1:63 ;
then ((((py `1 ) ^2 ) + ((py `2 ) ^2 )) / (1 + (((py `2 ) / (py `1 )) ^2 ))) * (1 + (((py `2 ) / (py `1 )) ^2 )) = 1 * (1 + (((py `2 ) / (py `1 )) ^2 )) by A192;
then ((py `1 ) ^2 ) + ((py `2 ) ^2 ) = 1 + (((py `2 ) / (py `1 )) ^2 ) by A204, XCMPLX_1:88;
then (((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1 = ((py `2 ) ^2 ) / ((py `1 ) ^2 ) by XCMPLX_1:77;
then ((((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1) * ((py `1 ) ^2 ) = (py `2 ) ^2 by A205, XCMPLX_1:6, XCMPLX_1:88;
hence ((((py `1 ) ^2 ) - 1) * ((py `1 ) ^2 )) + ((((py `1 ) ^2 ) - 1) * ((py `2 ) ^2 )) = 0 ; :: thesis: verum

end;

then A206: (((py `1 ) ^2 ) - 1) * (((py `1 ) ^2 ) + ((py `2 ) ^2 )) = 0 ;
((py `1 ) ^2 ) + ((py `2 ) ^2 ) <> 0 by A197, COMPLEX1:2;
then ((py `1 ) - 1) * ((py `1 ) + 1) = 0 by A206, XCMPLX_1:6;
then ( (py `1 ) - 1 = 0 or (py `1 ) + 1 = 0 ) by XCMPLX_1:6;
then A207: ( py `1 = 1 or py `1 = 0 - 1 ) ;
A208: gg . O = (Sq_Circ " ) . (g . O) by A4, FUNCT_1:22;
consider p3 being Point of (TOP-REAL 2) such that
A209: ( g . O = p3 & |.p3.| = 1 & p3 `2 <= p3 `1 & p3 `2 <= - (p3 `1 ) ) by A1;
A210: - (p3 `2 ) >= - (- (p3 `1 )) by A209, XREAL_1:26;
then A211: ( p3 <> 0. (TOP-REAL 2) & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) ) by A209, TOPRNS_1:24;
then A212: (Sq_Circ " ) . p3 = |[((p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by JGRAPH_3:40;
reconsider pz = gg . O as Point of (TOP-REAL 2) ;
A213: ( pz `2 = (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) & pz `1 = (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) by A208, A209, A212, EUCLID:56;
((p3 `1 ) / (p3 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p3 `1 ) / (p3 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A214: sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )) > 0 by SQUARE_1:93;

A215: now

assume A216: ( pz `2 = 0 & pz `1 = 0 ) ; :: thesis: contradiction
then A217: p3 `2 = 0 by A213, A214, XCMPLX_1:6;
p3 `1 = 0 by A213, A214, A216, XCMPLX_1:6;
hence contradiction by A211, A217, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A218: now

( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (- (p3 `2 )) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) ) by A209, A210, A214, XREAL_1:66;
then ( ( p3 `1 <= p3 `2 & (- (p3 `2 )) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A213, A214, XREAL_1:66;
hence ( ( (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) & - (pz `2 ) <= pz `1 ) or ( pz `1 >= pz `2 & pz `1 <= - (pz `2 ) ) ) by A213, A214, XREAL_1:66; :: thesis: verum

end;

A219: p3 = Sq_Circ . pz by A208, A209, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A220: Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A213, A215, A218, JGRAPH_2:11, JGRAPH_3:14;
A221: ( |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `2 = (pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) & |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| `1 = (pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ) by EUCLID:56;
((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
then A222: 1 + (((pz `1 ) / (pz `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
A223: pz `2 <> 0 by A213, A215, A218;
A224: |.p3.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A219, A220, A221, JGRAPH_3:10
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / ((sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))) ^2 )) by A222, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A222, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;

now

((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) * (1 + (((pz `1 ) / (pz `2 )) ^2 )) = 1 * (1 + (((pz `1 ) / (pz `2 )) ^2 )) by A209, A224;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) = 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A222, XCMPLX_1:88;
then (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1 = ((pz `1 ) ^2 ) / ((pz `2 ) ^2 ) by XCMPLX_1:77;
then ((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1) * ((pz `2 ) ^2 ) = (pz `1 ) ^2 by A223, XCMPLX_1:6, XCMPLX_1:88;
hence ((((pz `2 ) ^2 ) * (((pz `2 ) ^2 ) - 1)) + (((pz `2 ) ^2 ) * ((pz `1 ) ^2 ))) - (1 * ((pz `1 ) ^2 )) = 0 ; :: thesis: verum

end;

then A225: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) = 0 ;
((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A215, COMPLEX1:2;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) = 0 by A225, XCMPLX_1:6;
then ( (pz `2 ) - 1 = 0 or (pz `2 ) + 1 = 0 ) by XCMPLX_1:6;
then A226: ( pz `2 = 1 or pz `2 = 0 - 1 ) ;
A227: gg . I = (Sq_Circ " ) . (g . I) by A4, FUNCT_1:22;
consider p4 being Point of (TOP-REAL 2) such that
A228: ( g . I = p4 & |.p4.| = 1 & p4 `2 >= p4 `1 & p4 `2 >= - (p4 `1 ) ) by A1;
A229: - (p4 `2 ) <= - (- (p4 `1 )) by A228, XREAL_1:26;
then A230: ( p4 <> 0. (TOP-REAL 2) & ( ( p4 `1 <= p4 `2 & - (p4 `2 ) <= p4 `1 ) or ( p4 `1 >= p4 `2 & p4 `1 <= - (p4 `2 ) ) ) ) by A228, TOPRNS_1:24;
then A231: (Sq_Circ " ) . p4 = |[((p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )))),((p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))))]| by JGRAPH_3:40;
reconsider pu = gg . I as Point of (TOP-REAL 2) ;
A232: ( pu `2 = (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) & pu `1 = (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) ) by A227, A228, A231, EUCLID:56;
((p4 `1 ) / (p4 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p4 `1 ) / (p4 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A233: sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )) > 0 by SQUARE_1:93;

A234: now

assume A235: ( pu `2 = 0 & pu `1 = 0 ) ; :: thesis: contradiction
then A236: p4 `2 = 0 by A232, A233, XCMPLX_1:6;
p4 `1 = 0 by A232, A233, A235, XCMPLX_1:6;
hence contradiction by A230, A236, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A237: now

( ( p4 `1 <= p4 `2 & (- (p4 `2 )) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) <= (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) ) or ( pu `1 >= pu `2 & pu `1 <= - (pu `2 ) ) ) by A228, A229, A233, XREAL_1:66;
hence ( ( (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) <= (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) & - (pu `2 ) <= pu `1 ) or ( pu `1 >= pu `2 & pu `1 <= - (pu `2 ) ) ) by A232, A233, XREAL_1:66; :: thesis: verum

end;

A238: p4 = Sq_Circ . pu by A227, A228, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A239: Sq_Circ . pu = |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| by A232, A234, A237, JGRAPH_2:11, JGRAPH_3:14;
A240: ( |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| `2 = (pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) & |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| `1 = (pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ) by EUCLID:56;
((pu `1 ) / (pu `2 )) ^2 >= 0 by XREAL_1:65;
then A241: 1 + (((pu `1 ) / (pu `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
A242: pu `2 <> 0 by A232, A234, A237;

now

|.p4.| ^2 = (((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) + (((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) by A238, A239, A240, JGRAPH_3:10
.= (((pu `2 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) + (((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((pu `2 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) + (((pu `1 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((pu `2 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) + (((pu `1 ) ^2 ) / ((sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))) ^2 )) by A241, SQUARE_1:def 4
.= (((pu `2 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) + (((pu `1 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) by A241, SQUARE_1:def 4
.= (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) / (1 + (((pu `1 ) / (pu `2 )) ^2 )) by XCMPLX_1:63 ;
then ((((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) * (1 + (((pu `1 ) / (pu `2 )) ^2 )) = 1 * (1 + (((pu `1 ) / (pu `2 )) ^2 )) by A228;
then ((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) = 1 + (((pu `1 ) / (pu `2 )) ^2 ) by A241, XCMPLX_1:88;
then (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1 = ((pu `1 ) ^2 ) / ((pu `2 ) ^2 ) by XCMPLX_1:77;
then ((((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1) * ((pu `2 ) ^2 ) = (pu `1 ) ^2 by A242, XCMPLX_1:6, XCMPLX_1:88;
hence ((((pu `2 ) ^2 ) - 1) * ((pu `2 ) ^2 )) + ((((pu `2 ) ^2 ) - 1) * ((pu `1 ) ^2 )) = 0 ; :: thesis: verum

end;

then A243: (((pu `2 ) ^2 ) - 1) * (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) = 0 ;
((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) <> 0 by A234, COMPLEX1:2;
then ((pu `2 ) - 1) * ((pu `2 ) + 1) = 0 by A243, XCMPLX_1:6;
then ( (pu `2 ) - 1 = 0 or (pu `2 ) + 1 = 0 ) by XCMPLX_1:6;
then A244: ( pu `2 = 1 or pu `2 = 0 - 1 ) ;
thus ( - 1 <= (ff . O) `2 & (ff . O) `2 <= 1 ) by A177, A178, A182, A190, XREAL_1:66; :: thesis: ( - 1 <= (ff . I) `2 & (ff . I) `2 <= 1 & - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 & - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
thus ( - 1 <= (ff . I) `2 & (ff . I) `2 <= 1 ) by A195, A200, A207; :: thesis: ( - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 & - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
thus ( - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 ) by A213, A218, A226; :: thesis: ( - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
thus ( - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 ) by A232, A237, A244; :: thesis: verum

end;

then rng ff meets rng gg by A1, A7, A9, A10, A11, A12, A96, Th14;
then consider y being set such that
A245: ( y in rng ff & y in rng gg ) by XBOOLE_0:3;
consider x1 being set such that
A246: ( x1 in dom ff & y = ff . x1 ) by A245, FUNCT_1:def 5;
consider x2 being set such that
A247: ( x2 in dom gg & y = gg . x2 ) by A245, FUNCT_1:def 5;
A248: ff . x1 = (Sq_Circ " ) . (f . x1) by A246, FUNCT_1:22;
A249: dom (Sq_Circ " ) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1, JGRAPH_3:39;
x1 in dom f by A246, FUNCT_1:21;
then A250: f . x1 in rng f by FUNCT_1:def 5;
x2 in dom g by A247, FUNCT_1:21;
then A251: g . x2 in rng g by FUNCT_1:def 5;
A252: Sq_Circ " is one-to-one by JGRAPH_3:32;
gg . x2 = (Sq_Circ " ) . (g . x2) by A247, FUNCT_1:22;
then f . x1 = g . x2 by A246, A247, A248, A249, A250, A251, A252, FUNCT_1:def 8;
hence rng f meets rng g by A250, A251, XBOOLE_0:3; :: thesis: verum