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:13, JGRAPH_3:29;
reconsider ff = (Sq_Circ ") * f as Function of I[01],(TOP-REAL 2) by FUNCT_2:13, JGRAPH_3:29;
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:52;
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:52;
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:12;
then A13: p2 = Sq_Circ . py by A8, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A14: p2 <> 0. (TOP-REAL 2) by A9, TOPRNS_1:23;
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:28;
then A16: py `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A12, A8, EUCLID:52;
((p2 `2) / (p2 `1)) ^2 >= 0 by XREAL_1:63;
then A17: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by SQUARE_1:25;
A18: py `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A12, A8, A15, EUCLID:52;

A19: now :: thesis: ( py `1 = 0 implies not py `2 = 0 )

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:53, EUCLID:54; :: 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:64;
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:52, XREAL_1:64;
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:3, JGRAPH_3:def 1;
A22: ((py `2) / (py `1)) ^2 >= 0 by XREAL_1:63;
then A23: sqrt (1 + (((py `2) / (py `1)) ^2)) > 0 by SQUARE_1:25;

A24: now :: thesis: not py `1 = - 1

assume A25: py `1 = - 1 ; :: thesis: contradiction
- (p2 `2) <= - (- (p2 `1)) by A11, XREAL_1:24;
then - (p2 `2) < 0 by A13, A21, A7, A22, A25, SQUARE_1:25, XREAL_1:141;
then - (- (p2 `2)) > - 0 ;
hence contradiction by A10, A13, A21, A23, A25, EUCLID:52; :: 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:52;
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:1
.= (((py `1) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2)) + (((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((py `1) ^2) / (1 + (((py `2) / (py `1)) ^2))) + (((py `2) ^2) / (1 + (((py `2) / (py `1)) ^2))) by A22, SQUARE_1:def 2
.= (((py `1) ^2) + ((py `2) ^2)) / (1 + (((py `2) / (py `1)) ^2)) by XCMPLX_1:62 ;
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:87;
then A26: (((py `1) ^2) + ((py `2) ^2)) - 1 = ((py `2) ^2) / ((py `1) ^2) by XCMPLX_1:76;
py `1 <> 0 by A16, A18, A17, A19, A20, XREAL_1:64;
then ((((py `1) ^2) + ((py `2) ^2)) - 1) * ((py `1) ^2) = (py `2) ^2 by A26, XCMPLX_1:6, XCMPLX_1:87;
then A27: (((py `1) ^2) - 1) * (((py `1) ^2) + ((py `2) ^2)) = 0 ;
((py `1) ^2) + ((py `2) ^2) <> 0 by A19, COMPLEX1:1;
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:52;
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:63;
then A34: sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) > 0 by SQUARE_1:25;
A35: ff . O = (Sq_Circ ") . (f . O) by A4, FUNCT_1:12;
then A36: p1 = Sq_Circ . px by A30, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A37: p1 <> 0. (TOP-REAL 2) by A31, TOPRNS_1:23;
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:28;
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:52;

A39: now :: thesis: ( px `1 = 0 implies not px `2 = 0 )

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:53, EUCLID:54; :: 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:64;
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:64;
then ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) by A38, A34, XREAL_1:64;
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:3, JGRAPH_3:def 1;
A42: ((px `2) / (px `1)) ^2 >= 0 by XREAL_1:63;
then A43: sqrt (1 + (((px `2) / (px `1)) ^2)) > 0 by SQUARE_1:25;

A44: now :: thesis: not px `1 = 1

assume A45: px `1 = 1 ; :: thesis: contradiction
- (p1 `2) >= - (- (p1 `1)) by A33, XREAL_1:24;
then - (p1 `2) > 0 by A36, A41, A6, A43, A45, XREAL_1:139;
then - (- (p1 `2)) < - 0 ;
hence contradiction by A32, A36, A41, A43, A45, EUCLID:52; :: 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:52;
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:1
.= (((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2))) by A42, SQUARE_1:def 2
.= (((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2)) by XCMPLX_1:62 ;
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:87;
then A46: (((px `1) ^2) + ((px `2) ^2)) - 1 = ((px `2) ^2) / ((px `1) ^2) by XCMPLX_1:76;
px `1 <> 0 by A38, A34, A39, A40, XREAL_1:64;
then ((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) = (px `2) ^2 by A46, XCMPLX_1:6, XCMPLX_1:87;
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:52;
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:63;
then A53: sqrt (1 + (((p4 `1) / (p4 `2)) ^2)) > 0 by SQUARE_1:25;
A54: - (p4 `2) <= - (- (p4 `1)) by A52, XREAL_1:24;
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:64;
A56: gg . I = (Sq_Circ ") . (g . I) by A3, FUNCT_1:12;
then A57: p4 = Sq_Circ . pu by A49, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A58: p4 <> 0. (TOP-REAL 2) by A50, TOPRNS_1:23;
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:30;
then A60: pu `2 = (p4 `2) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))) by A56, A49, EUCLID:52;
A61: pu `1 = (p4 `1) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))) by A56, A49, A59, EUCLID:52;

A62: now :: thesis: ( pu `2 = 0 implies not pu `1 = 0 )

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:53, EUCLID:54; :: 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:52, XREAL_1:64;
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:3, JGRAPH_3:4;
A64: ((pu `1) / (pu `2)) ^2 >= 0 by XREAL_1:63;
then A65: sqrt (1 + (((pu `1) / (pu `2)) ^2)) > 0 by SQUARE_1:25;

A66: now :: thesis: not pu `2 = - 1

assume A67: pu `2 = - 1 ; :: thesis: contradiction
then - (p4 `1) < 0 by A52, A57, A63, A48, A64, SQUARE_1:25, XREAL_1:141;
then - (- (p4 `1)) > - 0 ;
hence contradiction by A51, A57, A63, A65, A67, EUCLID:52; :: 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:52;
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:1
.= (((pu `2) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2)) + (((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((pu `2) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) + (((pu `1) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) by A64, SQUARE_1:def 2
.= (((pu `2) ^2) + ((pu `1) ^2)) / (1 + (((pu `1) / (pu `2)) ^2)) by XCMPLX_1:62 ;
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:87;
then A68: (((pu `2) ^2) + ((pu `1) ^2)) - 1 = ((pu `1) ^2) / ((pu `2) ^2) by XCMPLX_1:76;
pu `2 <> 0 by A60, A61, A53, A62, A55, XREAL_1:64;
then ((((pu `2) ^2) + ((pu `1) ^2)) - 1) * ((pu `2) ^2) = (pu `1) ^2 by A68, XCMPLX_1:6, XCMPLX_1:87;
then A69: (((pu `2) ^2) - 1) * (((pu `2) ^2) + ((pu `1) ^2)) = 0 ;
((pu `2) ^2) + ((pu `1) ^2) <> 0 by A62, COMPLEX1:1;
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:23;
A76: gg . O = (Sq_Circ ") . (g . O) by A3, FUNCT_1:12;
then A77: p3 = Sq_Circ . pz by A71, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A78: - (p3 `2) >= - (- (p3 `1)) by A74, XREAL_1:24;
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:30;
then A80: pz `2 = (p3 `2) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))) by A76, A71, EUCLID:52;
((p3 `1) / (p3 `2)) ^2 >= 0 by XREAL_1:63;
then A81: sqrt (1 + (((p3 `1) / (p3 `2)) ^2)) > 0 by SQUARE_1:25;
A82: pz `1 = (p3 `1) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))) by A76, A71, A79, EUCLID:52;

A83: now :: thesis: ( pz `2 = 0 implies not pz `1 = 0 )

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:53, EUCLID:54; :: 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:64;
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:64;
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:52, XREAL_1:64;
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:3, JGRAPH_3:4;
A86: ((pz `1) / (pz `2)) ^2 >= 0 by XREAL_1:63;
then A87: sqrt (1 + (((pz `1) / (pz `2)) ^2)) > 0 by SQUARE_1:25;

A88: now :: thesis: not pz `2 = 1

assume A89: pz `2 = 1 ; :: thesis: contradiction
then - (p3 `1) > 0 by A74, A77, A85, A29, A87, XREAL_1:139;
then - (- (p3 `1)) < - 0 ;
hence contradiction by A73, A77, A85, A87, A89, EUCLID:52; :: 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:52;
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:1
.= (((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) by A86, SQUARE_1:def 2
.= (((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2)) by XCMPLX_1:62 ;
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:87;
then A90: (((pz `2) ^2) + ((pz `1) ^2)) - 1 = ((pz `1) ^2) / ((pz `2) ^2) by XCMPLX_1:76;
pz `2 <> 0 by A80, A82, A81, A83, A84, XREAL_1:64;
then ((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) = (pz `1) ^2 by A90, XCMPLX_1:6, XCMPLX_1:87;
then A91: (((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) = 0 ;
((pz `2) ^2) + ((pz `1) ^2) <> 0 by A83, COMPLEX1:1;
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:1;
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:3;
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:3;
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:12;

A100: now :: thesis: ( ( p2 = 0. (TOP-REAL 2) & contradiction ) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) & ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 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) ) & ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) ) )

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:23; :: 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:28;
then A103: px `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A99, A97, EUCLID:52;
set q = px;
A104: (px `1) ^2 >= 0 by XREAL_1:63;
|.p2.| ^2 >= |.p2.| by A98, XREAL_1:151;
then A105: |.p2.| ^2 >= 1 by A98, XXREAL_0:2;
A106: (px `2) ^2 >= 0 by XREAL_1:63;
((p2 `2) / (p2 `1)) ^2 >= 0 by XREAL_1:63;
then A107: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by SQUARE_1:25;
A108: px `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A99, A97, A102, EUCLID:52;

A109: now :: thesis: ( px `1 = 0 implies not px `2 = 0 )

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:53, EUCLID:54; :: 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:64;
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:64;
then A111: px `1 <> 0 by A103, A108, A107, A109, XREAL_1:64;
( ( (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:52, XREAL_1:64;
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:3, JGRAPH_3:def 1;
(Sq_Circ ") . p2 = px by A3, A97, FUNCT_1:12;
then A113: p2 = Sq_Circ . px by FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A114: ((px `2) / (px `1)) ^2 >= 0 by XREAL_1:63;
( |[((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:52;
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:1
.= (((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2))) by A114, SQUARE_1:def 2
.= (((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2)) by XCMPLX_1:62 ;
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:64;
then ((px `1) ^2) + ((px `2) ^2) >= 1 + (((px `2) / (px `1)) ^2) by A114, XCMPLX_1:87;
then ((px `1) ^2) + ((px `2) ^2) >= 1 + (((px `2) ^2) / ((px `1) ^2)) by XCMPLX_1:76;
then (((px `1) ^2) + ((px `2) ^2)) - 1 >= (1 + (((px `2) ^2) / ((px `1) ^2))) - 1 by XREAL_1:9;
then ((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) >= (((px `2) ^2) / ((px `1) ^2)) * ((px `1) ^2) by A104, XREAL_1:64;
then (((px `1) ^2) + (((px `2) ^2) - 1)) * ((px `1) ^2) >= (px `2) ^2 by A111, XCMPLX_1:6, XCMPLX_1:87;
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:9;
then A115: (((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) >= 0 ;
((px `1) ^2) + ((px `2) ^2) <> 0 by A109, COMPLEX1:1;
then ((px `1) - 1) * ((px `1) + 1) >= 0 by A104, A115, A106, XREAL_1:132;
hence ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) by XREAL_1:95; :: 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:28;
then A118: pz `2 = (p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by A99, A97, EUCLID:52;
((p2 `1) / (p2 `2)) ^2 >= 0 by XREAL_1:63;
then A119: sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0 by SQUARE_1:25;

A120: now :: thesis: ( pz `2 = 0 implies not pz `1 = 0 )

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:52;
( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ) by A116, JGRAPH_2:13;
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:64;
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:64;
then A124: pz `2 <> 0 by A118, A122, A119, A120, XREAL_1:64;
( ( (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:52, XREAL_1:64;
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:3, JGRAPH_3:4;
A126: ((pz `1) / (pz `2)) ^2 >= 0 by XREAL_1:63;
|.p2.| ^2 >= |.p2.| by A98, XREAL_1:151;
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:52;
A129: (pz `1) ^2 >= 0 by XREAL_1:63;
A130: (pz `2) ^2 >= 0 by XREAL_1:63;
( 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:52, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
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:1
.= (((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) by A126, SQUARE_1:def 2
.= (((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2)) by XCMPLX_1:62 ;
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:64;
then ((pz `2) ^2) + ((pz `1) ^2) >= 1 + (((pz `1) / (pz `2)) ^2) by A126, XCMPLX_1:87;
then ((pz `2) ^2) + ((pz `1) ^2) >= 1 + (((pz `1) ^2) / ((pz `2) ^2)) by XCMPLX_1:76;
then (((pz `2) ^2) + ((pz `1) ^2)) - 1 >= (1 + (((pz `1) ^2) / ((pz `2) ^2))) - 1 by XREAL_1:9;
then ((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) >= (((pz `1) ^2) / ((pz `2) ^2)) * ((pz `2) ^2) by A130, XREAL_1:64;
then (((pz `2) ^2) + (((pz `1) ^2) - 1)) * ((pz `2) ^2) >= (pz `1) ^2 by A124, XCMPLX_1:6, XCMPLX_1:87;
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:9;
then A131: (((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) >= 0 ;
((pz `2) ^2) + ((pz `1) ^2) <> 0 by A120, COMPLEX1:1;
then ((pz `2) - 1) * ((pz `2) + 1) >= 0 by A130, A131, A129, XREAL_1:132;
hence ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) by XREAL_1:95; :: thesis: verum

end;

end;

end;

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

now :: thesis: ( ( p1 = 0. (TOP-REAL 2) & contradiction ) or ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ) & ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 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) ) & ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) ) )

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:23; :: 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:28;
then A135: px `1 = (p1 `1) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) by A132, A95, EUCLID:52;
((p1 `2) / (p1 `1)) ^2 >= 0 by XREAL_1:63;
then A136: sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) > 0 by SQUARE_1:25;
A137: px `2 = (p1 `2) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) by A132, A95, A134, EUCLID:52;

A138: now :: thesis: ( px `1 = 0 implies not px `2 = 0 )

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:53, EUCLID:54; :: 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:64;
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:64;
then A140: px `1 <> 0 by A135, A137, A136, A138, XREAL_1:64;
|.p1.| ^2 >= |.p1.| by A96, XREAL_1:151;
then A141: |.p1.| ^2 >= 1 by A96, XXREAL_0:2;
A142: (px `1) ^2 >= 0 by XREAL_1:63;
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:52;
A144: (px `2) ^2 >= 0 by XREAL_1:63;
A145: ((px `2) / (px `1)) ^2 >= 0 by XREAL_1:63;
( ( (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:52, XREAL_1:64;
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:3, 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:52, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
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:1
.= (((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2))) by A145, SQUARE_1:def 2
.= (((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2)) by XCMPLX_1:62 ;
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:64;
then ((px `1) ^2) + ((px `2) ^2) >= 1 + (((px `2) / (px `1)) ^2) by A145, XCMPLX_1:87;
then ((px `1) ^2) + ((px `2) ^2) >= 1 + (((px `2) ^2) / ((px `1) ^2)) by XCMPLX_1:76;
then (((px `1) ^2) + ((px `2) ^2)) - 1 >= (1 + (((px `2) ^2) / ((px `1) ^2))) - 1 by XREAL_1:9;
then ((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) >= (((px `2) ^2) / ((px `1) ^2)) * ((px `1) ^2) by A142, XREAL_1:64;
then (((px `1) ^2) + (((px `2) ^2) - 1)) * ((px `1) ^2) >= (px `2) ^2 by A140, XCMPLX_1:6, XCMPLX_1:87;
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:9;
then A147: (((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) >= 0 ;
((px `1) ^2) + ((px `2) ^2) <> 0 by A138, COMPLEX1:1;
then ((px `1) - 1) * ((px `1) + 1) >= 0 by A142, A147, A144, XREAL_1:132;
hence ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) by XREAL_1:95; :: 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:28;
then A150: pz `2 = (p1 `2) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))) by A132, A95, EUCLID:52;
((p1 `1) / (p1 `2)) ^2 >= 0 by XREAL_1:63;
then A151: sqrt (1 + (((p1 `1) / (p1 `2)) ^2)) > 0 by SQUARE_1:25;

A152: now :: thesis: ( pz `2 = 0 implies not pz `1 = 0 )

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:52;
( ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) ) ) by A148, JGRAPH_2:13;
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:64;
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:64;
then A156: pz `2 <> 0 by A150, A154, A151, A152, XREAL_1:64;
( ( (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:52, XREAL_1:64;
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:3, JGRAPH_3:4;
A158: ((pz `1) / (pz `2)) ^2 >= 0 by XREAL_1:63;
|.p1.| ^2 >= |.p1.| by A96, XREAL_1:151;
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:52;
A161: (pz `1) ^2 >= 0 by XREAL_1:63;
A162: (pz `2) ^2 >= 0 by XREAL_1:63;
( 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:52, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
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:1
.= (((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) by A158, SQUARE_1:def 2
.= (((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2)) by XCMPLX_1:62 ;
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:64;
then ((pz `2) ^2) + ((pz `1) ^2) >= 1 + (((pz `1) / (pz `2)) ^2) by A158, XCMPLX_1:87;
then ((pz `2) ^2) + ((pz `1) ^2) >= 1 + (((pz `1) ^2) / ((pz `2) ^2)) by XCMPLX_1:76;
then (((pz `2) ^2) + ((pz `1) ^2)) - 1 >= (1 + (((pz `1) ^2) / ((pz `2) ^2))) - 1 by XREAL_1:9;
then ((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) >= (((pz `1) ^2) / ((pz `2) ^2)) * ((pz `2) ^2) by A162, XREAL_1:64;
then (((pz `2) ^2) + (((pz `1) ^2) - 1)) * ((pz `2) ^2) >= (pz `1) ^2 by A156, XCMPLX_1:6, XCMPLX_1:87;
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:9;
then A163: (((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) >= 0 ;
((pz `2) ^2) + ((pz `1) ^2) <> 0 by A152, COMPLEX1:1;
then ((pz `2) - 1) * ((pz `2) + 1) >= 0 by A162, A163, A161, XREAL_1:132;
hence ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) by XREAL_1:95; :: 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:52;
A165: ((px `2) / (px `1)) ^2 >= 0 by XREAL_1:63;
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:12;
then A170: p1 = Sq_Circ . px by A166, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
((p1 `2) / (p1 `1)) ^2 >= 0 by XREAL_1:63;
then A171: sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) > 0 by SQUARE_1:25;
A172: p1 <> 0. (TOP-REAL 2) by A167, TOPRNS_1:23;
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:28;
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:52;

A174: now :: thesis: ( px `1 = 0 implies not px `2 = 0 )

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:53, EUCLID:54; :: 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:64;
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:64;
then ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) by A173, A171, XREAL_1:64;
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:3, 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:1
.= (((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2))) by A165, SQUARE_1:def 2
.= (((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2)) by XCMPLX_1:62 ;
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:87;
then A176: (((px `1) ^2) + ((px `2) ^2)) - 1 = ((px `2) ^2) / ((px `1) ^2) by XCMPLX_1:76;
px `1 <> 0 by A173, A171, A174, A175, XREAL_1:64;
then ((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) = (px `2) ^2 by A176, XCMPLX_1:6, XCMPLX_1:87;
then A177: (((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) = 0 ;
((px `1) ^2) + ((px `2) ^2) <> 0 by A174, COMPLEX1:1;
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:64; :: 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:63;
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:52;
A180: ((pz `1) / (pz `2)) ^2 >= 0 by XREAL_1:63;
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:12;
then A185: p2 = Sq_Circ . py by A181, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A186: p2 <> 0. (TOP-REAL 2) by A182, TOPRNS_1:23;
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:28;
then A188: py `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A184, A181, EUCLID:52;
A189: py `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A184, A181, A187, EUCLID:52;
((p2 `2) / (p2 `1)) ^2 >= 0 by XREAL_1:63;
then A190: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by SQUARE_1:25;

A191: now :: thesis: ( py `1 = 0 implies not py `2 = 0 )

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:53, EUCLID:54; :: 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:64;
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:52, XREAL_1:64;
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:3, 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:1
.= (((py `1) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2)) + (((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((py `1) ^2) / (1 + (((py `2) / (py `1)) ^2))) + (((py `2) ^2) / (1 + (((py `2) / (py `1)) ^2))) by A178, SQUARE_1:def 2
.= (((py `1) ^2) + ((py `2) ^2)) / (1 + (((py `2) / (py `1)) ^2)) by XCMPLX_1:62 ;
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:87;
then A194: (((py `1) ^2) + ((py `2) ^2)) - 1 = ((py `2) ^2) / ((py `1) ^2) by XCMPLX_1:76;
py `1 <> 0 by A188, A189, A190, A191, A192, XREAL_1:64;
then ((((py `1) ^2) + ((py `2) ^2)) - 1) * ((py `1) ^2) = (py `2) ^2 by A194, XCMPLX_1:6, XCMPLX_1:87;
then A195: (((py `1) ^2) - 1) * (((py `1) ^2) + ((py `2) ^2)) = 0 ;
((py `1) ^2) + ((py `2) ^2) <> 0 by A191, COMPLEX1:1;
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:52;
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:23;
A202: gg . O = (Sq_Circ ") . (g . O) by A3, FUNCT_1:12;
then A203: p3 = Sq_Circ . pz by A197, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A204: - (p3 `2) >= - (- (p3 `1)) by A200, XREAL_1:24;
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:30;
then A206: pz `2 = (p3 `2) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))) by A202, A197, EUCLID:52;
A207: pz `1 = (p3 `1) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))) by A202, A197, A205, EUCLID:52;
((p3 `1) / (p3 `2)) ^2 >= 0 by XREAL_1:63;
then A208: sqrt (1 + (((p3 `1) / (p3 `2)) ^2)) > 0 by SQUARE_1:25;

A209: now :: thesis: ( pz `2 = 0 implies not pz `1 = 0 )

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:53, EUCLID:54; :: 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:64;
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:64;
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:52, XREAL_1:64;
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:3, JGRAPH_3:4;
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:1
.= (((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) by A180, SQUARE_1:def 2
.= (((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2)) by XCMPLX_1:62 ;
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:87;
then A212: (((pz `2) ^2) + ((pz `1) ^2)) - 1 = ((pz `1) ^2) / ((pz `2) ^2) by XCMPLX_1:76;
pz `2 <> 0 by A206, A207, A208, A209, A210, XREAL_1:64;
then ((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) = (pz `1) ^2 by A212, XCMPLX_1:6, XCMPLX_1:87;
then A213: (((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) = 0 ;
((pz `2) ^2) + ((pz `1) ^2) <> 0 by A209, COMPLEX1:1;
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:52;
A215: ((pu `1) / (pu `2)) ^2 >= 0 by XREAL_1:63;
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:24;
A221: gg . I = (Sq_Circ ") . (g . I) by A3, FUNCT_1:12;
then A222: p4 = Sq_Circ . pu by A216, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A223: p4 <> 0. (TOP-REAL 2) by A217, TOPRNS_1:23;
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:30;
then A225: pu `2 = (p4 `2) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))) by A221, A216, EUCLID:52;
A226: pu `1 = (p4 `1) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))) by A221, A216, A224, EUCLID:52;
((p4 `1) / (p4 `2)) ^2 >= 0 by XREAL_1:63;
then A227: sqrt (1 + (((p4 `1) / (p4 `2)) ^2)) > 0 by SQUARE_1:25;

A228: now :: thesis: ( pu `2 = 0 implies not pu `1 = 0 )

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:53, EUCLID:54; :: 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:64;
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:52, XREAL_1:64;
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:3, JGRAPH_3:4;
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:1
.= (((pu `2) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2)) + (((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((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 2
.= (((pu `2) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) + (((pu `1) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) by A215, SQUARE_1:def 2
.= (((pu `2) ^2) + ((pu `1) ^2)) / (1 + (((pu `1) / (pu `2)) ^2)) by XCMPLX_1:62 ;
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:87;
then A231: (((pu `2) ^2) + ((pu `1) ^2)) - 1 = ((pu `1) ^2) / ((pu `2) ^2) by XCMPLX_1:76;
pu `2 <> 0 by A225, A226, A227, A228, A229, XREAL_1:64;
then ((((pu `2) ^2) + ((pu `1) ^2)) - 1) * ((pu `2) ^2) = (pu `1) ^2 by A231, XCMPLX_1:6, XCMPLX_1:87;
then A232: (((pu `2) ^2) - 1) * (((pu `2) ^2) + ((pu `1) ^2)) = 0 ;
((pu `2) ^2) + ((pu `1) ^2) <> 0 by A228, COMPLEX1:1;
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, Th11, JGRAPH_3:22, JGRAPH_3:42;
then consider y being object such that
A233: y in rng ff and
A234: y in rng gg by XBOOLE_0:3;
consider x1 being object such that
A235: x1 in dom ff and
A236: y = ff . x1 by A233, FUNCT_1:def 3;
consider x2 being object such that
A237: x2 in dom gg and
A238: y = gg . x2 by A234, FUNCT_1:def 3;
A239: ( dom (Sq_Circ ") = the carrier of (TOP-REAL 2) & gg . x2 = (Sq_Circ ") . (g . x2) ) by A237, FUNCT_1:12, FUNCT_2:def 1, JGRAPH_3:29;
x1 in dom f by A235, FUNCT_1:11;
then A240: f . x1 in rng f by FUNCT_1:def 3;
x2 in dom g by A237, FUNCT_1:11;
then A241: g . x2 in rng g by FUNCT_1:def 3;
ff . x1 = (Sq_Circ ") . (f . x1) by A235, FUNCT_1:12;
then f . x1 = g . x2 by A236, A238, A240, A241, A239, FUNCT_1:def 4, JGRAPH_3:22;
hence rng f meets rng g by A240, A241, XBOOLE_0:3; :: thesis: verum