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
A2: dom g = the carrier of I[01] by FUNCT_2:def 1;
reconsider gg = (Sq_Circ " ) * g as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:19, JGRAPH_3:39;
reconsider ff = (Sq_Circ " ) * f as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:19, JGRAPH_3:39;
A3: dom gg = the carrier of I[01] by FUNCT_2:def 1;
A4: dom ff = the carrier of I[01] by FUNCT_2:def 1;
A5: ( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 )

proof

reconsider pz = gg . O as Point of (TOP-REAL 2) ;
reconsider py = ff . I as Point of (TOP-REAL 2) ;
reconsider px = ff . O as Point of (TOP-REAL 2) ;
set q = px;
A6: |[((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 ))) by EUCLID:56;
reconsider pu = gg . I as Point of (TOP-REAL 2) ;
A7: |[((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 ))) by EUCLID:56;
consider p2 being Point of (TOP-REAL 2) such that
A8: f . I = p2 and
A9: |.p2.| = 1 and
A10: p2 `2 <= p2 `1 and
A11: p2 `2 >= - (p2 `1 ) by A1;
A12: ff . I = (Sq_Circ " ) . (f . I) by A4, FUNCT_1:22;
then A13: p2 = Sq_Circ . py by A8, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A14: p2 <> 0. (TOP-REAL 2) by A9, TOPRNS_1:24;
then A15: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A10, A11, JGRAPH_3:38;
then A16: py `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A12, A8, EUCLID:56;
((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then A17: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;
A18: py `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A12, A8, A15, EUCLID:56;

A19: now

assume ( py `1 = 0 & py `2 = 0 ) ; :: thesis: contradiction
then ( p2 `1 = 0 & p2 `2 = 0 ) by A16, A18, A17, XCMPLX_1:6;
hence contradiction by A14, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A20: ( ( 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 A10, A11, A17, XREAL_1:66;
then ( ( (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 A12, A8, A15, A16, A17, EUCLID:56, XREAL_1:66;
then A21: Sq_Circ . py = |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| by A16, A18, A19, JGRAPH_2:11, JGRAPH_3:def 1;
A22: ((py `2 ) / (py `1 )) ^2 >= 0 by XREAL_1:65;
then A23: sqrt (1 + (((py `2 ) / (py `1 )) ^2 )) > 0 by SQUARE_1:93;

A24: now

assume A25: py `1 = - 1 ; :: thesis: contradiction
- (p2 `2 ) <= - (- (p2 `1 )) by A11, XREAL_1:26;
then - (p2 `2 ) < 0 by A13, A21, A7, A22, A25, SQUARE_1:93, XREAL_1:143;
then - (- (p2 `2 )) > - 0 ;
hence contradiction by A10, A13, A21, A23, A25, EUCLID:56; :: thesis: verum

end;

|[((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;
then |.p2.| ^2 = (((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) + (((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) by A13, A21, A7, 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 A22, SQUARE_1:def 4
.= (((py `1 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) + (((py `2 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) by A22, 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 A9;
then ((py `1 ) ^2 ) + ((py `2 ) ^2 ) = 1 + (((py `2 ) / (py `1 )) ^2 ) by A22, XCMPLX_1:88;
then A26: (((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1 = ((py `2 ) ^2 ) / ((py `1 ) ^2 ) by XCMPLX_1:77;
py `1 <> 0 by A16, A18, A17, A19, A20, XREAL_1:66;
then ((((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1) * ((py `1 ) ^2 ) = (py `2 ) ^2 by A26, XCMPLX_1:6, XCMPLX_1:88;
then A27: (((py `1 ) ^2 ) - 1) * (((py `1 ) ^2 ) + ((py `2 ) ^2 )) = 0 ;
((py `1 ) ^2 ) + ((py `2 ) ^2 ) <> 0 by A19, COMPLEX1:2;
then ((py `1 ) - 1) * ((py `1 ) + 1) = 0 by A27, XCMPLX_1:6;
then A28: ( (py `1 ) - 1 = 0 or (py `1 ) + 1 = 0 ) by XCMPLX_1:6;
A29: |[((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 ))) by EUCLID:56;
consider p1 being Point of (TOP-REAL 2) such that
A30: f . O = p1 and
A31: |.p1.| = 1 and
A32: p1 `2 >= p1 `1 and
A33: p1 `2 <= - (p1 `1 ) by A1;
((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then A34: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by SQUARE_1:93;
A35: ff . O = (Sq_Circ " ) . (f . O) by A4, FUNCT_1:22;
then A36: p1 = Sq_Circ . px by A30, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A37: p1 <> 0. (TOP-REAL 2) by A31, TOPRNS_1:24;
then (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by A32, A33, JGRAPH_3:38;
then A38: ( px `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & px `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A35, A30, EUCLID:56;

A39: now

assume ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then ( p1 `1 = 0 & p1 `2 = 0 ) by A38, A34, XCMPLX_1:6;
hence contradiction by A37, 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 A32, A33, A34, XREAL_1:66;
then A40: ( ( 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 A38, A34, XREAL_1:66;
then ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A38, A34, XREAL_1:66;
then A41: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A39, JGRAPH_2:11, JGRAPH_3:def 1;
A42: ((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
then A43: sqrt (1 + (((px `2 ) / (px `1 )) ^2 )) > 0 by SQUARE_1:93;

A44: now

assume A45: px `1 = 1 ; :: thesis: contradiction
- (p1 `2 ) >= - (- (p1 `1 )) by A33, XREAL_1:26;
then - (p1 `2 ) > 0 by A36, A41, A6, A43, A45, XREAL_1:141;
then - (- (p1 `2 )) < - 0 ;
hence contradiction by A32, A36, A41, A43, A45, EUCLID:56; :: thesis: verum

end;

|[((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;
then |.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A36, A41, A6, 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 A42, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A42, 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 A31;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) = 1 + (((px `2 ) / (px `1 )) ^2 ) by A42, XCMPLX_1:88;
then A46: (((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1 = ((px `2 ) ^2 ) / ((px `1 ) ^2 ) by XCMPLX_1:77;
px `1 <> 0 by A38, A34, A39, A40, XREAL_1:66;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1) * ((px `1 ) ^2 ) = (px `2 ) ^2 by A46, XCMPLX_1:6, XCMPLX_1:88;
then A47: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) = 0 ;
A48: |[((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 ))) by EUCLID:56;
consider p4 being Point of (TOP-REAL 2) such that
A49: g . I = p4 and
A50: |.p4.| = 1 and
A51: p4 `2 >= p4 `1 and
A52: p4 `2 >= - (p4 `1 ) by A1;
((p4 `1 ) / (p4 `2 )) ^2 >= 0 by XREAL_1:65;
then A53: sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )) > 0 by SQUARE_1:93;
A54: - (p4 `2 ) <= - (- (p4 `1 )) by A52, XREAL_1:26;
then A55: ( ( 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 A51, A53, XREAL_1:66;
A56: gg . I = (Sq_Circ " ) . (g . I) by A3, FUNCT_1:22;
then A57: p4 = Sq_Circ . pu by A49, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A58: p4 <> 0. (TOP-REAL 2) by A50, TOPRNS_1:24;
then A59: (Sq_Circ " ) . p4 = |[((p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )))),((p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))))]| by A51, A54, JGRAPH_3:40;
then A60: pu `2 = (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) by A56, A49, EUCLID:56;
A61: pu `1 = (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) by A56, A49, A59, EUCLID:56;

A62: now

assume ( pu `2 = 0 & pu `1 = 0 ) ; :: thesis: contradiction
then ( p4 `2 = 0 & p4 `1 = 0 ) by A60, A61, A53, XCMPLX_1:6;
hence contradiction by A58, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( (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 A56, A49, A59, A60, A53, A55, EUCLID:56, XREAL_1:66;
then A63: Sq_Circ . pu = |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| by A60, A61, A62, JGRAPH_2:11, JGRAPH_3:14;
A64: ((pu `1 ) / (pu `2 )) ^2 >= 0 by XREAL_1:65;
then A65: sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )) > 0 by SQUARE_1:93;

A66: now

assume A67: pu `2 = - 1 ; :: thesis: contradiction
then - (p4 `1 ) < 0 by A52, A57, A63, A48, A64, SQUARE_1:93, XREAL_1:143;
then - (- (p4 `1 )) > - 0 ;
hence contradiction by A51, A57, A63, A65, A67, EUCLID:56; :: thesis: verum

end;

|[((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;
then |.p4.| ^2 = (((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) + (((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) by A57, A63, A48, 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 A64, SQUARE_1:def 4
.= (((pu `2 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) + (((pu `1 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) by A64, 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 A50;
then ((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) = 1 + (((pu `1 ) / (pu `2 )) ^2 ) by A64, XCMPLX_1:88;
then A68: (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1 = ((pu `1 ) ^2 ) / ((pu `2 ) ^2 ) by XCMPLX_1:77;
pu `2 <> 0 by A60, A61, A53, A62, A55, XREAL_1:66;
then ((((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1) * ((pu `2 ) ^2 ) = (pu `1 ) ^2 by A68, XCMPLX_1:6, XCMPLX_1:88;
then A69: (((pu `2 ) ^2 ) - 1) * (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) = 0 ;
((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) <> 0 by A62, COMPLEX1:2;
then ((pu `2 ) - 1) * ((pu `2 ) + 1) = 0 by A69, XCMPLX_1:6;
then A70: ( (pu `2 ) - 1 = 0 or (pu `2 ) + 1 = 0 ) by XCMPLX_1:6;
consider p3 being Point of (TOP-REAL 2) such that
A71: g . O = p3 and
A72: |.p3.| = 1 and
A73: p3 `2 <= p3 `1 and
A74: p3 `2 <= - (p3 `1 ) by A1;
A75: p3 <> 0. (TOP-REAL 2) by A72, TOPRNS_1:24;
A76: gg . O = (Sq_Circ " ) . (g . O) by A3, FUNCT_1:22;
then A77: p3 = Sq_Circ . pz by A71, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A78: - (p3 `2 ) >= - (- (p3 `1 )) by A74, XREAL_1:26;
then A79: (Sq_Circ " ) . p3 = |[((p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A73, A75, JGRAPH_3:40;
then A80: pz `2 = (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) by A76, A71, EUCLID:56;
((p3 `1 ) / (p3 `2 )) ^2 >= 0 by XREAL_1:65;
then A81: sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )) > 0 by SQUARE_1:93;
A82: pz `1 = (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) by A76, A71, A79, EUCLID:56;

A83: now

assume ( pz `2 = 0 & pz `1 = 0 ) ; :: thesis: contradiction
then ( p3 `2 = 0 & p3 `1 = 0 ) by A80, A82, A81, XCMPLX_1:6;
hence contradiction by A75, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( 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 A73, A78, A81, XREAL_1:66;
then A84: ( ( 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 A80, A82, A81, XREAL_1:66;
then ( ( (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 A76, A71, A79, A80, A81, EUCLID:56, XREAL_1:66;
then A85: Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A80, A82, A83, JGRAPH_2:11, JGRAPH_3:14;
A86: ((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
then A87: sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )) > 0 by SQUARE_1:93;

A88: now

assume A89: pz `2 = 1 ; :: thesis: contradiction
then - (p3 `1 ) > 0 by A74, A77, A85, A29, A87, XREAL_1:141;
then - (- (p3 `1 )) < - 0 ;
hence contradiction by A73, A77, A85, A87, A89, EUCLID:56; :: thesis: verum

end;

|[((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;
then |.p3.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A77, A85, A29, 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 A86, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A86, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;
then ((((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 A72;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) = 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A86, XCMPLX_1:88;
then A90: (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1 = ((pz `1 ) ^2 ) / ((pz `2 ) ^2 ) by XCMPLX_1:77;
pz `2 <> 0 by A80, A82, A81, A83, A84, XREAL_1:66;
then ((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1) * ((pz `2 ) ^2 ) = (pz `1 ) ^2 by A90, XCMPLX_1:6, XCMPLX_1:88;
then A91: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) = 0 ;
((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A83, COMPLEX1:2;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) = 0 by A91, XCMPLX_1:6;
then A92: ( (pz `2 ) - 1 = 0 or (pz `2 ) + 1 = 0 ) by XCMPLX_1:6;
((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A39, COMPLEX1:2;
then ((px `1 ) - 1) * ((px `1 ) + 1) = 0 by A47, XCMPLX_1:6;
then ( (px `1 ) - 1 = 0 or (px `1 ) + 1 = 0 ) by XCMPLX_1:6;
hence ( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 ) by A44, A28, A24, A92, A88, A70, A66; :: thesis: verum

end;

A93: dom f = the carrier of I[01] by FUNCT_2:def 1;
A94: 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 ) )
f . r in rng f by A93, FUNCT_1:12;
then f . r in C0 by A1;
then consider p1 being Point of (TOP-REAL 2) such that
A95: f . r = p1 and
A96: |.p1.| >= 1 by A1;
g . r in rng g by A2, FUNCT_1:12;
then g . r in C0 by A1;
then consider p2 being Point of (TOP-REAL 2) such that
A97: g . r = p2 and
A98: |.p2.| >= 1 by A1;
A99: gg . r = (Sq_Circ " ) . (g . r) by A3, FUNCT_1:22;

A100: 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 A98, TOPRNS_1:24; :: thesis: verum

end;

case A101: ( 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 )

reconsider px = gg . r as Point of (TOP-REAL 2) ;
A102: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A101, JGRAPH_3:38;
then A103: px `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A99, A97, EUCLID:56;
set q = px;
A104: (px `1 ) ^2 >= 0 by XREAL_1:65;
|.p2.| ^2 >= |.p2.| by A98, XREAL_1:153;
then A105: |.p2.| ^2 >= 1 by A98, XXREAL_0:2;
A106: (px `2 ) ^2 >= 0 by XREAL_1:65;
((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then A107: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;
A108: px `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A99, A97, A102, EUCLID:56;

A109: now

assume ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then ( p2 `1 = 0 & p2 `2 = 0 ) by A103, A108, A107, XCMPLX_1:6;
hence contradiction by A101, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( 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 A101, A107, XREAL_1:66;
then A110: ( ( 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 A103, A108, A107, XREAL_1:66;
then A111: px `1 <> 0 by A103, A108, A107, A109, XREAL_1:66;
( ( (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 A99, A97, A102, A103, A107, A110, EUCLID:56, XREAL_1:66;
then A112: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A103, A108, A109, JGRAPH_2:11, JGRAPH_3:def 1;
(Sq_Circ " ) . p2 = px by A3, A97, FUNCT_1:22;
then A113: p2 = Sq_Circ . px by FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A114: ((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
( |[((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;
then |.p2.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A113, A112, 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 A114, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A114, 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 A114, A105, XREAL_1:66;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 1 + (((px `2 ) / (px `1 )) ^2 ) by A114, 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 A104, XREAL_1:66;
then (((px `1 ) ^2 ) + (((px `2 ) ^2 ) - 1)) * ((px `1 ) ^2 ) >= (px `2 ) ^2 by A111, 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;
then A115: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) >= 0 ;
((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A109, COMPLEX1:2;
then ((px `1 ) - 1) * ((px `1 ) + 1) >= 0 by A104, A115, A106, 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 A116: ( 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 )

reconsider pz = gg . r as Point of (TOP-REAL 2) ;
A117: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A116, JGRAPH_3:38;
then A118: pz `2 = (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A99, A97, EUCLID:56;
((p2 `1 ) / (p2 `2 )) ^2 >= 0 by XREAL_1:65;
then A119: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by SQUARE_1:93;

A120: now

assume that
A121: pz `2 = 0 and
pz `1 = 0 ; :: thesis: contradiction
p2 `2 = 0 by A118, A119, A121, XCMPLX_1:6;
hence contradiction by A116; :: thesis: verum

end;

A122: pz `1 = (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A99, A97, A117, EUCLID:56;
( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) by A116, JGRAPH_2:23;
then ( ( 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 A119, XREAL_1:66;
then A123: ( ( 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 A118, A122, A119, XREAL_1:66;
then A124: pz `2 <> 0 by A118, A122, A119, A120, XREAL_1:66;
( ( (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 A99, A97, A117, A118, A119, A123, EUCLID:56, XREAL_1:66;
then A125: Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A118, A122, A120, JGRAPH_2:11, JGRAPH_3:14;
A126: ((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
|.p2.| ^2 >= |.p2.| by A98, XREAL_1:153;
then A127: |.p2.| ^2 >= 1 by A98, XXREAL_0:2;
A128: |[((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;
A129: (pz `1 ) ^2 >= 0 by XREAL_1:65;
A130: (pz `2 ) ^2 >= 0 by XREAL_1:65;
( p2 = Sq_Circ . pz & |[((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 ))) ) by A99, A97, EUCLID:56, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
then |.p2.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A125, A128, 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 A126, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A126, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;
then ((((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 A126, A127, XREAL_1:66;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A126, 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 A130, XREAL_1:66;
then (((pz `2 ) ^2 ) + (((pz `1 ) ^2 ) - 1)) * ((pz `2 ) ^2 ) >= (pz `1 ) ^2 by A124, 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;
then A131: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) >= 0 ;
((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A120, COMPLEX1:2;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) >= 0 by A130, A131, A129, 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;

A132: ff . r = (Sq_Circ " ) . (f . r) by A4, FUNCT_1:22;

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 A96, TOPRNS_1:24; :: thesis: verum

end;

case A133: ( 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 )

reconsider px = ff . r as Point of (TOP-REAL 2) ;
A134: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by A133, JGRAPH_3:38;
then A135: px `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A132, A95, EUCLID:56;
((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then A136: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by SQUARE_1:93;
A137: px `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A132, A95, A134, EUCLID:56;

A138: now

assume ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then ( p1 `1 = 0 & p1 `2 = 0 ) by A135, A137, A136, XCMPLX_1:6;
hence contradiction by A133, 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 A133, A136, XREAL_1:66;
then A139: ( ( 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 A135, A137, A136, XREAL_1:66;
then A140: px `1 <> 0 by A135, A137, A136, A138, XREAL_1:66;
|.p1.| ^2 >= |.p1.| by A96, XREAL_1:153;
then A141: |.p1.| ^2 >= 1 by A96, XXREAL_0:2;
A142: (px `1 ) ^2 >= 0 by XREAL_1:65;
set q = px;
A143: |[((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;
A144: (px `2 ) ^2 >= 0 by XREAL_1:65;
A145: ((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
( ( (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 A132, A95, A134, A135, A136, A139, EUCLID:56, XREAL_1:66;
then A146: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A135, A137, A138, JGRAPH_2:11, JGRAPH_3:def 1;
( p1 = Sq_Circ . px & |[((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 ))) ) by A132, A95, EUCLID:56, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
then |.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A146, A143, 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 A145, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A145, 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 A145, A141, XREAL_1:66;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 1 + (((px `2 ) / (px `1 )) ^2 ) by A145, 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 A142, XREAL_1:66;
then (((px `1 ) ^2 ) + (((px `2 ) ^2 ) - 1)) * ((px `1 ) ^2 ) >= (px `2 ) ^2 by A140, 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;
then A147: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) >= 0 ;
((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A138, COMPLEX1:2;
then ((px `1 ) - 1) * ((px `1 ) + 1) >= 0 by A142, A147, A144, 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 A148: ( 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 )

reconsider pz = ff . r as Point of (TOP-REAL 2) ;
A149: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| by A148, JGRAPH_3:38;
then A150: pz `2 = (p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A132, A95, EUCLID:56;
((p1 `1 ) / (p1 `2 )) ^2 >= 0 by XREAL_1:65;
then A151: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) > 0 by SQUARE_1:93;

A152: now

assume that
A153: pz `2 = 0 and
pz `1 = 0 ; :: thesis: contradiction
p1 `2 = 0 by A150, A151, A153, XCMPLX_1:6;
hence contradiction by A148; :: thesis: verum

end;

A154: pz `1 = (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A132, A95, A149, EUCLID:56;
( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2 ) ) ) by A148, JGRAPH_2:23;
then ( ( 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 A151, XREAL_1:66;
then A155: ( ( 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 A150, A154, A151, XREAL_1:66;
then A156: pz `2 <> 0 by A150, A154, A151, A152, XREAL_1:66;
( ( (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 A132, A95, A149, A150, A151, A155, EUCLID:56, XREAL_1:66;
then A157: Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A150, A154, A152, JGRAPH_2:11, JGRAPH_3:14;
A158: ((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
|.p1.| ^2 >= |.p1.| by A96, XREAL_1:153;
then A159: |.p1.| ^2 >= 1 by A96, XXREAL_0:2;
A160: |[((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;
A161: (pz `1 ) ^2 >= 0 by XREAL_1:65;
A162: (pz `2 ) ^2 >= 0 by XREAL_1:65;
( p1 = Sq_Circ . pz & |[((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 ))) ) by A132, A95, EUCLID:56, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
then |.p1.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A157, A160, 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 A158, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A158, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;
then ((((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 A158, A159, XREAL_1:66;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) >= 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A158, 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 A162, XREAL_1:66;
then (((pz `2 ) ^2 ) + (((pz `1 ) ^2 ) - 1)) * ((pz `2 ) ^2 ) >= (pz `1 ) ^2 by A156, 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;
then A163: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) >= 0 ;
((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A152, COMPLEX1:2;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) >= 0 by A162, A163, A161, 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;

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 A100; :: 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

reconsider pz = gg . O as Point of (TOP-REAL 2) ;
reconsider py = ff . I as Point of (TOP-REAL 2) ;
reconsider px = ff . O as Point of (TOP-REAL 2) ;
set q = px;
A164: ( |[((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;
A165: ((px `2 ) / (px `1 )) ^2 >= 0 by XREAL_1:65;
consider p1 being Point of (TOP-REAL 2) such that
A166: f . O = p1 and
A167: |.p1.| = 1 and
A168: ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) by A1;
A169: ff . O = (Sq_Circ " ) . (f . O) by A4, FUNCT_1:22;
then A170: p1 = Sq_Circ . px by A166, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then A171: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by SQUARE_1:93;
A172: p1 <> 0. (TOP-REAL 2) by A167, TOPRNS_1:24;
then (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by A168, JGRAPH_3:38;
then A173: ( px `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & px `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A169, A166, EUCLID:56;

A174: now

assume ( px `1 = 0 & px `2 = 0 ) ; :: thesis: contradiction
then ( p1 `1 = 0 & p1 `2 = 0 ) by A173, A171, XCMPLX_1:6;
hence contradiction by A172, 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 A168, A171, XREAL_1:66;
then A175: ( ( 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 A173, A171, XREAL_1:66;
then ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) by A173, A171, XREAL_1:66;
then Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by A174, JGRAPH_2:11, JGRAPH_3:def 1;
then |.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A170, A164, 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 A165, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A165, 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 A167;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) = 1 + (((px `2 ) / (px `1 )) ^2 ) by A165, XCMPLX_1:88;
then A176: (((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1 = ((px `2 ) ^2 ) / ((px `1 ) ^2 ) by XCMPLX_1:77;
px `1 <> 0 by A173, A171, A174, A175, XREAL_1:66;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1) * ((px `1 ) ^2 ) = (px `2 ) ^2 by A176, XCMPLX_1:6, XCMPLX_1:88;
then A177: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) = 0 ;
((px `1 ) ^2 ) + ((px `2 ) ^2 ) <> 0 by A174, COMPLEX1:2;
then ((px `1 ) - 1) * ((px `1 ) + 1) = 0 by A177, XCMPLX_1:6;
then ( (px `1 ) - 1 = 0 or (px `1 ) + 1 = 0 ) by XCMPLX_1:6;
then ( px `1 = 1 or px `1 = 0 - 1 ) ;
hence ( - 1 <= (ff . O) `2 & (ff . O) `2 <= 1 ) by A173, A171, A175, 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 )
A178: ((py `2 ) / (py `1 )) ^2 >= 0 by XREAL_1:65;
reconsider pu = gg . I as Point of (TOP-REAL 2) ;
A179: ( |[((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;
A180: ((pz `1 ) / (pz `2 )) ^2 >= 0 by XREAL_1:65;
consider p2 being Point of (TOP-REAL 2) such that
A181: f . I = p2 and
A182: |.p2.| = 1 and
A183: ( p2 `2 <= p2 `1 & p2 `2 >= - (p2 `1 ) ) by A1;
A184: ff . I = (Sq_Circ " ) . (f . I) by A4, FUNCT_1:22;
then A185: p2 = Sq_Circ . py by A181, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A186: p2 <> 0. (TOP-REAL 2) by A182, TOPRNS_1:24;
then A187: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A183, JGRAPH_3:38;
then A188: py `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A184, A181, EUCLID:56;
A189: py `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A184, A181, A187, EUCLID:56;
((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then A190: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;

A191: now

assume ( py `1 = 0 & py `2 = 0 ) ; :: thesis: contradiction
then ( p2 `1 = 0 & p2 `2 = 0 ) by A188, A189, A190, XCMPLX_1:6;
hence contradiction by A186, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A192: ( ( 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 A183, A190, XREAL_1:66;
then A193: ( ( (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 A184, A181, A187, A188, A190, EUCLID:56, XREAL_1:66;
then Sq_Circ . py = |[((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| by A188, A189, A191, JGRAPH_2:11, JGRAPH_3:def 1;
then |.p2.| ^2 = (((py `1 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) + (((py `2 ) / (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))) ^2 ) by A185, A179, 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 A178, SQUARE_1:def 4
.= (((py `1 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) + (((py `2 ) ^2 ) / (1 + (((py `2 ) / (py `1 )) ^2 ))) by A178, 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 A182;
then ((py `1 ) ^2 ) + ((py `2 ) ^2 ) = 1 + (((py `2 ) / (py `1 )) ^2 ) by A178, XCMPLX_1:88;
then A194: (((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1 = ((py `2 ) ^2 ) / ((py `1 ) ^2 ) by XCMPLX_1:77;
py `1 <> 0 by A188, A189, A190, A191, A192, XREAL_1:66;
then ((((py `1 ) ^2 ) + ((py `2 ) ^2 )) - 1) * ((py `1 ) ^2 ) = (py `2 ) ^2 by A194, XCMPLX_1:6, XCMPLX_1:88;
then A195: (((py `1 ) ^2 ) - 1) * (((py `1 ) ^2 ) + ((py `2 ) ^2 )) = 0 ;
((py `1 ) ^2 ) + ((py `2 ) ^2 ) <> 0 by A191, COMPLEX1:2;
then ((py `1 ) - 1) * ((py `1 ) + 1) = 0 by A195, XCMPLX_1:6;
then ( (py `1 ) - 1 = 0 or (py `1 ) + 1 = 0 ) by XCMPLX_1:6;
hence ( - 1 <= (ff . I) `2 & (ff . I) `2 <= 1 ) by A188, A189, A193; :: thesis: ( - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 & - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
A196: ( |[((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;
consider p3 being Point of (TOP-REAL 2) such that
A197: g . O = p3 and
A198: |.p3.| = 1 and
A199: p3 `2 <= p3 `1 and
A200: p3 `2 <= - (p3 `1 ) by A1;
A201: p3 <> 0. (TOP-REAL 2) by A198, TOPRNS_1:24;
A202: gg . O = (Sq_Circ " ) . (g . O) by A3, FUNCT_1:22;
then A203: p3 = Sq_Circ . pz by A197, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A204: - (p3 `2 ) >= - (- (p3 `1 )) by A200, XREAL_1:26;
then A205: (Sq_Circ " ) . p3 = |[((p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A199, A201, JGRAPH_3:40;
then A206: pz `2 = (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) by A202, A197, EUCLID:56;
A207: pz `1 = (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) by A202, A197, A205, EUCLID:56;
((p3 `1 ) / (p3 `2 )) ^2 >= 0 by XREAL_1:65;
then A208: sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )) > 0 by SQUARE_1:93;

A209: now

assume ( pz `2 = 0 & pz `1 = 0 ) ; :: thesis: contradiction
then ( p3 `2 = 0 & p3 `1 = 0 ) by A206, A207, A208, XCMPLX_1:6;
hence contradiction by A201, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( 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 A199, A204, A208, XREAL_1:66;
then A210: ( ( 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 A206, A207, A208, XREAL_1:66;
then A211: ( ( (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 A202, A197, A205, A206, A208, EUCLID:56, XREAL_1:66;
then Sq_Circ . pz = |[((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))),((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 ))))]| by A206, A207, A209, JGRAPH_2:11, JGRAPH_3:14;
then |.p3.| ^2 = (((pz `2 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) + (((pz `1 ) / (sqrt (1 + (((pz `1 ) / (pz `2 )) ^2 )))) ^2 ) by A203, A196, 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 A180, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) + (((pz `1 ) ^2 ) / (1 + (((pz `1 ) / (pz `2 )) ^2 ))) by A180, SQUARE_1:def 4
.= (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) / (1 + (((pz `1 ) / (pz `2 )) ^2 )) by XCMPLX_1:63 ;
then ((((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 A198;
then ((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) = 1 + (((pz `1 ) / (pz `2 )) ^2 ) by A180, XCMPLX_1:88;
then A212: (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1 = ((pz `1 ) ^2 ) / ((pz `2 ) ^2 ) by XCMPLX_1:77;
pz `2 <> 0 by A206, A207, A208, A209, A210, XREAL_1:66;
then ((((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) - 1) * ((pz `2 ) ^2 ) = (pz `1 ) ^2 by A212, XCMPLX_1:6, XCMPLX_1:88;
then A213: (((pz `2 ) ^2 ) - 1) * (((pz `2 ) ^2 ) + ((pz `1 ) ^2 )) = 0 ;
((pz `2 ) ^2 ) + ((pz `1 ) ^2 ) <> 0 by A209, COMPLEX1:2;
then ((pz `2 ) - 1) * ((pz `2 ) + 1) = 0 by A213, XCMPLX_1:6;
then ( (pz `2 ) - 1 = 0 or (pz `2 ) + 1 = 0 ) by XCMPLX_1:6;
hence ( - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 ) by A206, A207, A211; :: thesis: ( - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
A214: ( |[((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;
A215: ((pu `1 ) / (pu `2 )) ^2 >= 0 by XREAL_1:65;
consider p4 being Point of (TOP-REAL 2) such that
A216: g . I = p4 and
A217: |.p4.| = 1 and
A218: p4 `2 >= p4 `1 and
A219: p4 `2 >= - (p4 `1 ) by A1;
A220: - (p4 `2 ) <= - (- (p4 `1 )) by A219, XREAL_1:26;
A221: gg . I = (Sq_Circ " ) . (g . I) by A3, FUNCT_1:22;
then A222: p4 = Sq_Circ . pu by A216, FUNCT_1:54, JGRAPH_3:32, JGRAPH_3:54;
A223: p4 <> 0. (TOP-REAL 2) by A217, TOPRNS_1:24;
then A224: (Sq_Circ " ) . p4 = |[((p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )))),((p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))))]| by A218, A220, JGRAPH_3:40;
then A225: pu `2 = (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) by A221, A216, EUCLID:56;
A226: pu `1 = (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) by A221, A216, A224, EUCLID:56;
((p4 `1 ) / (p4 `2 )) ^2 >= 0 by XREAL_1:65;
then A227: sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )) > 0 by SQUARE_1:93;

A228: now

assume ( pu `2 = 0 & pu `1 = 0 ) ; :: thesis: contradiction
then ( p4 `2 = 0 & p4 `1 = 0 ) by A225, A226, A227, XCMPLX_1:6;
hence contradiction by A223, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A229: ( ( 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 A218, A220, A227, XREAL_1:66;
then A230: ( ( (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 A221, A216, A224, A225, A227, EUCLID:56, XREAL_1:66;
then Sq_Circ . pu = |[((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))),((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 ))))]| by A225, A226, A228, JGRAPH_2:11, JGRAPH_3:14;
then |.p4.| ^2 = (((pu `2 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) + (((pu `1 ) / (sqrt (1 + (((pu `1 ) / (pu `2 )) ^2 )))) ^2 ) by A222, A214, 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 A215, SQUARE_1:def 4
.= (((pu `2 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) + (((pu `1 ) ^2 ) / (1 + (((pu `1 ) / (pu `2 )) ^2 ))) by A215, 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 A217;
then ((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) = 1 + (((pu `1 ) / (pu `2 )) ^2 ) by A215, XCMPLX_1:88;
then A231: (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1 = ((pu `1 ) ^2 ) / ((pu `2 ) ^2 ) by XCMPLX_1:77;
pu `2 <> 0 by A225, A226, A227, A228, A229, XREAL_1:66;
then ((((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) - 1) * ((pu `2 ) ^2 ) = (pu `1 ) ^2 by A231, XCMPLX_1:6, XCMPLX_1:88;
then A232: (((pu `2 ) ^2 ) - 1) * (((pu `2 ) ^2 ) + ((pu `1 ) ^2 )) = 0 ;
((pu `2 ) ^2 ) + ((pu `1 ) ^2 ) <> 0 by A228, COMPLEX1:2;
then ((pu `2 ) - 1) * ((pu `2 ) + 1) = 0 by A232, XCMPLX_1:6;
then ( (pu `2 ) - 1 = 0 or (pu `2 ) + 1 = 0 ) by XCMPLX_1:6;
hence ( - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 ) by A225, A226, A230; :: thesis: verum

end;

then rng ff meets rng gg by A1, A5, A94, Th14, JGRAPH_3:32, JGRAPH_3:52;
then consider y being set such that
A233: y in rng ff and
A234: y in rng gg by XBOOLE_0:3;
consider x1 being set such that
A235: x1 in dom ff and
A236: y = ff . x1 by A233, FUNCT_1:def 5;
consider x2 being set such that
A237: x2 in dom gg and
A238: y = gg . x2 by A234, FUNCT_1:def 5;
A239: ( dom (Sq_Circ " ) = the carrier of (TOP-REAL 2) & gg . x2 = (Sq_Circ " ) . (g . x2) ) by A237, FUNCT_1:22, FUNCT_2:def 1, JGRAPH_3:39;
x1 in dom f by A235, FUNCT_1:21;
then A240: f . x1 in rng f by FUNCT_1:def 5;
x2 in dom g by A237, FUNCT_1:21;
then A241: g . x2 in rng g by FUNCT_1:def 5;
ff . x1 = (Sq_Circ " ) . (f . x1) by A235, FUNCT_1:22;
then f . x1 = g . x2 by A236, A238, A240, A241, A239, FUNCT_1:def 8, JGRAPH_3:32;
hence rng f meets rng g by A240, A241, XBOOLE_0:3; :: thesis: verum