A1: dom (Sq_Circ " ) = the carrier of (TOP-REAL 2) by Th39, FUNCT_2:def 1;
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 A2: ( 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
then consider p1 being Point of (TOP-REAL 2) such that
A3: f . O = p1 and
A4: |.p1.| = 1 and
A5: p1 `2 >= p1 `1 and
A6: p1 `2 <= - (p1 `1 ) ;
reconsider gg = (Sq_Circ " ) * g as Function of I[01] ,(TOP-REAL 2) by Th39, FUNCT_2:19;
A7: dom g = the carrier of I[01] by FUNCT_2:def 1;
reconsider ff = (Sq_Circ " ) * f as Function of I[01] ,(TOP-REAL 2) by Th39, FUNCT_2:19;
A8: dom gg = the carrier of I[01] by FUNCT_2:def 1;
A9: dom ff = the carrier of I[01] by FUNCT_2:def 1;
then A10: ff . O = (Sq_Circ " ) . (f . O) by FUNCT_1:22;
A11: dom f = the carrier of I[01] by FUNCT_2:def 1;
A12: for r being Point of I[01] holds
( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 )

proof

let r be Point of I[01] ; :: thesis: ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 )
f . r in rng f by A11, FUNCT_1:12;
then f . r in C0 by A2;
then consider p1 being Point of (TOP-REAL 2) such that
A13: f . r = p1 and
A14: |.p1.| <= 1 by A2;
g . r in rng g by A7, FUNCT_1:12;
then g . r in C0 by A2;
then consider p2 being Point of (TOP-REAL 2) such that
A15: g . r = p2 and
A16: |.p2.| <= 1 by A2;
A17: gg . r = (Sq_Circ " ) . (g . r) by A8, FUNCT_1:22;

A18: 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: ( - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 )

hence ( - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) by A17, A15, Th38, JGRAPH_2:11; :: thesis: verum

end;

case A19: ( 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 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 )

set px = gg . r;
A20: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A19, Th38;
then A21: (gg . r) `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A17, A15, EUCLID:56;
|.p2.| ^2 <= |.p2.| by A16, SQUARE_1:111;
then A22: |.p2.| ^2 <= 1 by A16, XXREAL_0:2;
A23: ((gg . r) `2 ) ^2 >= 0 by XREAL_1:65;
A24: ((gg . r) `1 ) ^2 >= 0 by XREAL_1:65;
A25: (gg . r) `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A17, A15, A20, EUCLID:56;
A26: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
then ( ( 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 A19, XREAL_1:66;
then A27: ( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( (gg . r) `2 >= (gg . r) `1 & (gg . r) `2 <= - ((gg . r) `1 ) ) ) by A21, A25, A26, XREAL_1:66;
then A28: ( ( (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & - ((gg . r) `1 ) <= (gg . r) `2 ) or ( (gg . r) `2 >= (gg . r) `1 & (gg . r) `2 <= - ((gg . r) `1 ) ) ) by A17, A15, A20, A21, A26, EUCLID:56, XREAL_1:66;

A29: now

assume ( (gg . r) `1 = 0 & (gg . r) `2 = 0 ) ; :: thesis: contradiction
then ( p2 `1 = 0 & p2 `2 = 0 ) by A21, A25, A26, XCMPLX_1:6;
hence contradiction by A19, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A30: (gg . r) `1 <> 0 by A21, A25, A26, A27, XREAL_1:66;
set q = gg . r;
A31: |[(((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )))),(((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))))]| `2 = ((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) by EUCLID:56;
A32: 1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ) > 0 by Lm1;
A33: ( p2 = Sq_Circ . (gg . r) & |[(((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )))),(((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))))]| `1 = ((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) ) by A17, A15, Th54, EUCLID:56, FUNCT_1:54;
Sq_Circ . (gg . r) = |[(((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )))),(((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))))]| by A21, A25, A29, A28, Def1, JGRAPH_2:11;
then |.p2.| ^2 = ((((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )))) ^2 ) + ((((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )))) ^2 ) by A33, A31, JGRAPH_1:46
.= ((((gg . r) `1 ) ^2 ) / ((sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) ^2 )) + ((((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((gg . r) `1 ) ^2 ) / ((sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) ^2 )) + ((((gg . r) `2 ) ^2 ) / ((sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((gg . r) `1 ) ^2 ) / (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) + ((((gg . r) `2 ) ^2 ) / ((sqrt (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) ^2 )) by A32, SQUARE_1:def 4
.= ((((gg . r) `1 ) ^2 ) / (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) + ((((gg . r) `2 ) ^2 ) / (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) by A32, SQUARE_1:def 4
.= ((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) / (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )) by XCMPLX_1:63 ;
then (((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) / (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ))) * (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )) <= 1 * (1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 )) by A32, A22, XREAL_1:66;
then (((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 ) <= 1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ) by A32, XCMPLX_1:88;
then (((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 ) <= 1 + ((((gg . r) `2 ) ^2 ) / (((gg . r) `1 ) ^2 )) by XCMPLX_1:77;
then ((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) - 1 <= (((gg . r) `2 ) ^2 ) / (((gg . r) `1 ) ^2 ) by XREAL_1:22;
then (((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) - 1) * (((gg . r) `1 ) ^2 ) <= ((((gg . r) `2 ) ^2 ) / (((gg . r) `1 ) ^2 )) * (((gg . r) `1 ) ^2 ) by A24, XREAL_1:66;
then (((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) - 1) * (((gg . r) `1 ) ^2 ) <= ((gg . r) `2 ) ^2 by A30, XCMPLX_1:6, XCMPLX_1:88;
then A34: ((((gg . r) `1 ) ^2 ) - 1) * ((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) <= 0 by Lm19;
(((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 ) <> 0 by A29, COMPLEX1:2;
then A35: (((gg . r) `1 ) ^2 ) - 1 <= 0 by A24, A34, A23, XREAL_1:131;
then A36: (gg . r) `1 >= - 1 by SQUARE_1:112;
A37: (gg . r) `1 <= 1 by A35, SQUARE_1:112;
then ( ( (gg . r) `2 <= 1 & - (- ((gg . r) `1 )) >= - ((gg . r) `2 ) ) or ( (gg . r) `2 >= - 1 & (gg . r) `2 <= - ((gg . r) `1 ) ) ) by A21, A25, A28, A36, XREAL_1:26, XXREAL_0:2;
then ( ( (gg . r) `2 <= 1 & (gg . r) `1 >= - ((gg . r) `2 ) ) or ( (gg . r) `2 >= - 1 & - ((gg . r) `2 ) >= - (- ((gg . r) `1 )) ) ) by XREAL_1:26;
then ( ( (gg . r) `2 <= 1 & 1 >= - ((gg . r) `2 ) ) or ( (gg . r) `2 >= - 1 & - ((gg . r) `2 ) >= (gg . r) `1 ) ) by A37, XXREAL_0:2;
then ( ( (gg . r) `2 <= 1 & - 1 <= - (- ((gg . r) `2 )) ) or ( (gg . r) `2 >= - 1 & - ((gg . r) `2 ) >= - 1 ) ) by A36, XREAL_1:26, XXREAL_0:2;
hence ( - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) by A35, SQUARE_1:112, XREAL_1:26; :: thesis: verum

end;

case A38: ( 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 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 )

set pz = gg . r;
A39: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A38, Th38;
then A40: (gg . r) `2 = (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A17, A15, EUCLID:56;
A41: (gg . r) `1 = (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A17, A15, A39, EUCLID:56;
A42: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) by A38, 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 A42, XREAL_1:66;
then A43: ( ( p2 `1 <= p2 `2 & (- (p2 `2 )) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) or ( (gg . r) `1 >= (gg . r) `2 & (gg . r) `1 <= - ((gg . r) `2 ) ) ) by A40, A41, A42, XREAL_1:66;
then A44: ( ( (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) & - ((gg . r) `2 ) <= (gg . r) `1 ) or ( (gg . r) `1 >= (gg . r) `2 & (gg . r) `1 <= - ((gg . r) `2 ) ) ) by A17, A15, A39, A40, A42, EUCLID:56, XREAL_1:66;

A45: now

assume that
A46: (gg . r) `2 = 0 and
(gg . r) `1 = 0 ; :: thesis: contradiction
p2 `2 = 0 by A40, A42, A46, XCMPLX_1:6;
hence contradiction by A38; :: thesis: verum

end;

then A47: (gg . r) `2 <> 0 by A40, A41, A42, A43, XREAL_1:66;
A48: ( p2 = Sq_Circ . (gg . r) & |[(((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )))),(((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))))]| `2 = ((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) ) by A17, A15, Th54, EUCLID:56, FUNCT_1:54;
A49: ((gg . r) `2 ) ^2 >= 0 by XREAL_1:65;
|.p2.| ^2 <= |.p2.| by A16, SQUARE_1:111;
then A50: |.p2.| ^2 <= 1 by A16, XXREAL_0:2;
A51: ((gg . r) `1 ) ^2 >= 0 by XREAL_1:65;
A52: |[(((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )))),(((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))))]| `1 = ((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) by EUCLID:56;
A53: 1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ) > 0 by Lm1;
Sq_Circ . (gg . r) = |[(((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )))),(((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))))]| by A40, A41, A45, A44, Th14, JGRAPH_2:11;
then |.p2.| ^2 = ((((gg . r) `2 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )))) ^2 ) + ((((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )))) ^2 ) by A48, A52, JGRAPH_1:46
.= ((((gg . r) `2 ) ^2 ) / ((sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) ^2 )) + ((((gg . r) `1 ) / (sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((gg . r) `2 ) ^2 ) / ((sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) ^2 )) + ((((gg . r) `1 ) ^2 ) / ((sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((gg . r) `2 ) ^2 ) / (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) + ((((gg . r) `1 ) ^2 ) / ((sqrt (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) ^2 )) by A53, SQUARE_1:def 4
.= ((((gg . r) `2 ) ^2 ) / (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) + ((((gg . r) `1 ) ^2 ) / (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) by A53, SQUARE_1:def 4
.= ((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) / (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )) by XCMPLX_1:63 ;
then (((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) / (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ))) * (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )) <= 1 * (1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 )) by A53, A50, XREAL_1:66;
then (((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 ) <= 1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ) by A53, XCMPLX_1:88;
then (((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 ) <= 1 + ((((gg . r) `1 ) ^2 ) / (((gg . r) `2 ) ^2 )) by XCMPLX_1:77;
then ((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) - 1 <= (((gg . r) `1 ) ^2 ) / (((gg . r) `2 ) ^2 ) by XREAL_1:22;
then (((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) - 1) * (((gg . r) `2 ) ^2 ) <= ((((gg . r) `1 ) ^2 ) / (((gg . r) `2 ) ^2 )) * (((gg . r) `2 ) ^2 ) by A49, XREAL_1:66;
then (((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) - 1) * (((gg . r) `2 ) ^2 ) <= ((gg . r) `1 ) ^2 by A47, XCMPLX_1:6, XCMPLX_1:88;
then A54: ((((gg . r) `2 ) ^2 ) - 1) * ((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) <= 0 by Lm19;
(((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 ) <> 0 by A45, COMPLEX1:2;
then A55: (((gg . r) `2 ) ^2 ) - 1 <= 0 by A49, A54, A51, XREAL_1:131;
then A56: (gg . r) `2 >= - 1 by SQUARE_1:112;
A57: (gg . r) `2 <= 1 by A55, SQUARE_1:112;
then ( ( (gg . r) `1 <= 1 & - (- ((gg . r) `2 )) >= - ((gg . r) `1 ) ) or ( (gg . r) `1 >= - 1 & (gg . r) `1 <= - ((gg . r) `2 ) ) ) by A40, A41, A44, A56, XREAL_1:26, XXREAL_0:2;
then ( ( (gg . r) `1 <= 1 & 1 >= - ((gg . r) `1 ) ) or ( (gg . r) `1 >= - 1 & - ((gg . r) `1 ) >= - (- ((gg . r) `2 )) ) ) by A57, XREAL_1:26, XXREAL_0:2;
then ( ( (gg . r) `1 <= 1 & 1 >= - ((gg . r) `1 ) ) or ( (gg . r) `1 >= - 1 & - ((gg . r) `1 ) >= - 1 ) ) by A56, XXREAL_0:2;
then ( ( (gg . r) `1 <= 1 & - 1 <= - (- ((gg . r) `1 )) ) or ( (gg . r) `1 >= - 1 & (gg . r) `1 <= 1 ) ) by XREAL_1:26;
hence ( - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) by A55, SQUARE_1:112; :: thesis: verum

end;

end;

end;

A58: ff . r = (Sq_Circ " ) . (f . r) by A9, 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: ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 )

hence ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 ) by A58, A13, Th38, JGRAPH_2:11; :: thesis: verum

end;

case A59: ( 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 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 )

set px = ff . r;
(Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by A59, Th38;
then A60: ( (ff . r) `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & (ff . r) `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A58, A13, EUCLID:56;
A61: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
then ( ( 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 A59, XREAL_1:66;
then A62: ( ( p1 `2 <= p1 `1 & (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) or ( (ff . r) `2 >= (ff . r) `1 & (ff . r) `2 <= - ((ff . r) `1 ) ) ) by A60, A61, XREAL_1:66;
then A63: ( ( (ff . r) `2 <= (ff . r) `1 & - ((ff . r) `1 ) <= (ff . r) `2 ) or ( (ff . r) `2 >= (ff . r) `1 & (ff . r) `2 <= - ((ff . r) `1 ) ) ) by A60, A61, XREAL_1:66;

A64: now

assume ( (ff . r) `1 = 0 & (ff . r) `2 = 0 ) ; :: thesis: contradiction
then ( p1 `1 = 0 & p1 `2 = 0 ) by A60, A61, XCMPLX_1:6;
hence contradiction by A59, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A65: (ff . r) `1 <> 0 by A60, A61, A62, XREAL_1:66;
|.p1.| ^2 <= |.p1.| by A14, SQUARE_1:111;
then A66: |.p1.| ^2 <= 1 by A14, XXREAL_0:2;
A67: ((ff . r) `1 ) ^2 >= 0 by XREAL_1:65;
A68: ((ff . r) `2 ) ^2 >= 0 by XREAL_1:65;
set q = ff . r;
A69: |[(((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )))),(((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))))]| `2 = ((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) by EUCLID:56;
A70: 1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ) > 0 by Lm1;
A71: ( p1 = Sq_Circ . (ff . r) & |[(((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )))),(((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))))]| `1 = ((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) ) by A58, A13, Th54, EUCLID:56, FUNCT_1:54;
Sq_Circ . (ff . r) = |[(((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )))),(((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))))]| by A64, A63, Def1, JGRAPH_2:11;
then |.p1.| ^2 = ((((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )))) ^2 ) + ((((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )))) ^2 ) by A71, A69, JGRAPH_1:46
.= ((((ff . r) `1 ) ^2 ) / ((sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) ^2 )) + ((((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((ff . r) `1 ) ^2 ) / ((sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) ^2 )) + ((((ff . r) `2 ) ^2 ) / ((sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((ff . r) `1 ) ^2 ) / (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) + ((((ff . r) `2 ) ^2 ) / ((sqrt (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) ^2 )) by A70, SQUARE_1:def 4
.= ((((ff . r) `1 ) ^2 ) / (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) + ((((ff . r) `2 ) ^2 ) / (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) by A70, SQUARE_1:def 4
.= ((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) / (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )) by XCMPLX_1:63 ;
then (((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) / (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ))) * (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )) <= 1 * (1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 )) by A70, A66, XREAL_1:66;
then (((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 ) <= 1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ) by A70, XCMPLX_1:88;
then (((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 ) <= 1 + ((((ff . r) `2 ) ^2 ) / (((ff . r) `1 ) ^2 )) by XCMPLX_1:77;
then ((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) - 1 <= (((ff . r) `2 ) ^2 ) / (((ff . r) `1 ) ^2 ) by XREAL_1:22;
then (((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) - 1) * (((ff . r) `1 ) ^2 ) <= ((((ff . r) `2 ) ^2 ) / (((ff . r) `1 ) ^2 )) * (((ff . r) `1 ) ^2 ) by A67, XREAL_1:66;
then (((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) - 1) * (((ff . r) `1 ) ^2 ) <= ((ff . r) `2 ) ^2 by A65, XCMPLX_1:6, XCMPLX_1:88;
then A72: ((((ff . r) `1 ) ^2 ) - 1) * ((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) <= 0 by Lm19;
(((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 ) <> 0 by A64, COMPLEX1:2;
then A73: (((ff . r) `1 ) ^2 ) - 1 <= 0 by A67, A72, A68, XREAL_1:131;
then A74: (ff . r) `1 >= - 1 by SQUARE_1:112;
A75: (ff . r) `1 <= 1 by A73, SQUARE_1:112;
then ( ( (ff . r) `2 <= 1 & - (- ((ff . r) `1 )) >= - ((ff . r) `2 ) ) or ( (ff . r) `2 >= - 1 & (ff . r) `2 <= - ((ff . r) `1 ) ) ) by A63, A74, XREAL_1:26, XXREAL_0:2;
then ( ( (ff . r) `2 <= 1 & (ff . r) `1 >= - ((ff . r) `2 ) ) or ( (ff . r) `2 >= - 1 & - ((ff . r) `2 ) >= - (- ((ff . r) `1 )) ) ) by XREAL_1:26;
then ( ( (ff . r) `2 <= 1 & 1 >= - ((ff . r) `2 ) ) or ( (ff . r) `2 >= - 1 & - ((ff . r) `2 ) >= (ff . r) `1 ) ) by A75, XXREAL_0:2;
then ( ( (ff . r) `2 <= 1 & - 1 <= - (- ((ff . r) `2 )) ) or ( (ff . r) `2 >= - 1 & - ((ff . r) `2 ) >= - 1 ) ) by A74, XREAL_1:26, XXREAL_0:2;
hence ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 ) by A73, SQUARE_1:112, XREAL_1:26; :: thesis: verum

end;

case A76: ( 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 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 )

set pz = ff . r;
A77: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| by A76, Th38;
then A78: (ff . r) `2 = (p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A58, A13, EUCLID:56;
A79: (ff . r) `1 = (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A58, A13, A77, EUCLID:56;
A80: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2 ) ) ) by A76, 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 A80, XREAL_1:66;
then A81: ( ( p1 `1 <= p1 `2 & (- (p1 `2 )) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) <= (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) or ( (ff . r) `1 >= (ff . r) `2 & (ff . r) `1 <= - ((ff . r) `2 ) ) ) by A78, A79, A80, XREAL_1:66;
then A82: ( ( (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) & - ((ff . r) `2 ) <= (ff . r) `1 ) or ( (ff . r) `1 >= (ff . r) `2 & (ff . r) `1 <= - ((ff . r) `2 ) ) ) by A58, A13, A77, A78, A80, EUCLID:56, XREAL_1:66;

A83: now

assume that
A84: (ff . r) `2 = 0 and
(ff . r) `1 = 0 ; :: thesis: contradiction
p1 `2 = 0 by A78, A80, A84, XCMPLX_1:6;
hence contradiction by A76; :: thesis: verum

end;

then A85: (ff . r) `2 <> 0 by A78, A79, A80, A81, XREAL_1:66;
A86: ( p1 = Sq_Circ . (ff . r) & |[(((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )))),(((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))))]| `2 = ((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) ) by A58, A13, Th54, EUCLID:56, FUNCT_1:54;
A87: ((ff . r) `2 ) ^2 >= 0 by XREAL_1:65;
|.p1.| ^2 <= |.p1.| by A14, SQUARE_1:111;
then A88: |.p1.| ^2 <= 1 by A14, XXREAL_0:2;
A89: ((ff . r) `1 ) ^2 >= 0 by XREAL_1:65;
A90: |[(((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )))),(((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))))]| `1 = ((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) by EUCLID:56;
A91: 1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ) > 0 by Lm1;
Sq_Circ . (ff . r) = |[(((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )))),(((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))))]| by A78, A79, A83, A82, Th14, JGRAPH_2:11;
then |.p1.| ^2 = ((((ff . r) `2 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )))) ^2 ) + ((((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )))) ^2 ) by A86, A90, JGRAPH_1:46
.= ((((ff . r) `2 ) ^2 ) / ((sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) ^2 )) + ((((ff . r) `1 ) / (sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((ff . r) `2 ) ^2 ) / ((sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) ^2 )) + ((((ff . r) `1 ) ^2 ) / ((sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((ff . r) `2 ) ^2 ) / (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) + ((((ff . r) `1 ) ^2 ) / ((sqrt (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) ^2 )) by A91, SQUARE_1:def 4
.= ((((ff . r) `2 ) ^2 ) / (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) + ((((ff . r) `1 ) ^2 ) / (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) by A91, SQUARE_1:def 4
.= ((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) / (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )) by XCMPLX_1:63 ;
then (((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) / (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ))) * (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )) <= 1 * (1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 )) by A91, A88, XREAL_1:66;
then (((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 ) <= 1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ) by A91, XCMPLX_1:88;
then (((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 ) <= 1 + ((((ff . r) `1 ) ^2 ) / (((ff . r) `2 ) ^2 )) by XCMPLX_1:77;
then ((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) - 1 <= (((ff . r) `1 ) ^2 ) / (((ff . r) `2 ) ^2 ) by XREAL_1:22;
then (((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) - 1) * (((ff . r) `2 ) ^2 ) <= ((((ff . r) `1 ) ^2 ) / (((ff . r) `2 ) ^2 )) * (((ff . r) `2 ) ^2 ) by A87, XREAL_1:66;
then (((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) - 1) * (((ff . r) `2 ) ^2 ) <= ((ff . r) `1 ) ^2 by A85, XCMPLX_1:6, XCMPLX_1:88;
then A92: ((((ff . r) `2 ) ^2 ) - 1) * ((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) <= 0 by Lm19;
(((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 ) <> 0 by A83, COMPLEX1:2;
then A93: (((ff . r) `2 ) ^2 ) - 1 <= 0 by A87, A92, A89, XREAL_1:131;
then A94: (ff . r) `2 >= - 1 by SQUARE_1:112;
A95: (ff . r) `2 <= 1 by A93, SQUARE_1:112;
then ( ( (ff . r) `1 <= 1 & - (- ((ff . r) `2 )) >= - ((ff . r) `1 ) ) or ( (ff . r) `1 >= - 1 & (ff . r) `1 <= - ((ff . r) `2 ) ) ) by A78, A79, A82, A94, XREAL_1:26, XXREAL_0:2;
then ( ( (ff . r) `1 <= 1 & 1 >= - ((ff . r) `1 ) ) or ( (ff . r) `1 >= - 1 & - ((ff . r) `1 ) >= - (- ((ff . r) `2 )) ) ) by A95, XREAL_1:26, XXREAL_0:2;
then ( ( (ff . r) `1 <= 1 & 1 >= - ((ff . r) `1 ) ) or ( (ff . r) `1 >= - 1 & - ((ff . r) `1 ) >= - 1 ) ) by A94, XXREAL_0:2;
then ( ( (ff . r) `1 <= 1 & - 1 <= - (- ((ff . r) `1 )) ) or ( (ff . r) `1 >= - 1 & (ff . r) `1 <= 1 ) ) by XREAL_1:26;
hence ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 ) by A93, SQUARE_1:112; :: thesis: verum

end;

end;

end;

hence ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) by A18; :: thesis: verum

end;

consider y being Element of (rng ff) /\ (rng gg);
A96: p1 <> 0. (TOP-REAL 2) by A4, TOPRNS_1:24;
then A97: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by A5, A6, Th38;
( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 )

proof

set pz = gg . O;
set py = ff . I;
set px = ff . O;
set q = ff . O;
A98: |[(((ff . O) `1 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )))),(((ff . O) `2 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))))]| `1 = ((ff . O) `1 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) by EUCLID:56;
set pu = gg . I;
A99: |[(((ff . I) `1 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )))),(((ff . I) `2 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))))]| `1 = ((ff . I) `1 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) by EUCLID:56;
A100: |[(((gg . I) `1 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )))),(((gg . I) `2 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))))]| `2 = ((gg . I) `2 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) by EUCLID:56;
A101: 1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ) > 0 by Lm1;
(Sq_Circ " ) . p1 = ff . O by A9, A3, FUNCT_1:22;
then A102: p1 = Sq_Circ . (ff . O) by Th54, FUNCT_1:54;
consider p4 being Point of (TOP-REAL 2) such that
A103: g . I = p4 and
A104: |.p4.| = 1 and
A105: p4 `2 >= p4 `1 and
A106: p4 `2 >= - (p4 `1 ) by A2;
A107: sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A108: - (p4 `2 ) <= - (- (p4 `1 )) by A106, XREAL_1:26;
then A109: ( ( p4 `1 <= p4 `2 & (- (p4 `2 )) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) <= (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) ) or ( (gg . I) `1 >= (gg . I) `2 & (gg . I) `1 <= - ((gg . I) `2 ) ) ) by A105, A107, XREAL_1:66;
A110: gg . I = (Sq_Circ " ) . (g . I) by A8, FUNCT_1:22;
then A111: p4 = Sq_Circ . (gg . I) by A103, Th54, FUNCT_1:54;
A112: p4 <> 0. (TOP-REAL 2) by A104, TOPRNS_1:24;
then A113: (Sq_Circ " ) . p4 = |[((p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )))),((p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))))]| by A105, A108, Th40;
then A114: (gg . I) `2 = (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) by A110, A103, EUCLID:56;
A115: (gg . I) `1 = (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) by A110, A103, A113, EUCLID:56;

A116: now

assume ( (gg . I) `2 = 0 & (gg . I) `1 = 0 ) ; :: thesis: contradiction
then ( p4 `2 = 0 & p4 `1 = 0 ) by A114, A115, A107, XCMPLX_1:6;
hence contradiction by A112, 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 ))) & - ((gg . I) `2 ) <= (gg . I) `1 ) or ( (gg . I) `1 >= (gg . I) `2 & (gg . I) `1 <= - ((gg . I) `2 ) ) ) by A110, A103, A113, A114, A107, A109, EUCLID:56, XREAL_1:66;
then A117: Sq_Circ . (gg . I) = |[(((gg . I) `1 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )))),(((gg . I) `2 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))))]| by A114, A115, A116, Th14, JGRAPH_2:11;
|[(((gg . I) `1 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )))),(((gg . I) `2 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))))]| `1 = ((gg . I) `1 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) by EUCLID:56;
then |.p4.| ^2 = ((((gg . I) `2 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )))) ^2 ) + ((((gg . I) `1 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )))) ^2 ) by A111, A117, A100, JGRAPH_1:46
.= ((((gg . I) `2 ) ^2 ) / ((sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) ^2 )) + ((((gg . I) `1 ) / (sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((gg . I) `2 ) ^2 ) / ((sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) ^2 )) + ((((gg . I) `1 ) ^2 ) / ((sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((gg . I) `2 ) ^2 ) / (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) + ((((gg . I) `1 ) ^2 ) / ((sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) ^2 )) by A101, SQUARE_1:def 4
.= ((((gg . I) `2 ) ^2 ) / (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) + ((((gg . I) `1 ) ^2 ) / (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) by A101, SQUARE_1:def 4
.= ((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) / (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )) by XCMPLX_1:63 ;
then (((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) / (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ))) * (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )) = 1 * (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )) by A104;
then (((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 ) = 1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ) by A101, XCMPLX_1:88;
then A118: ((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) - 1 = (((gg . I) `1 ) ^2 ) / (((gg . I) `2 ) ^2 ) by XCMPLX_1:77;
(gg . I) `2 <> 0 by A114, A115, A107, A116, A109, XREAL_1:66;
then (((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) - 1) * (((gg . I) `2 ) ^2 ) = ((gg . I) `1 ) ^2 by A118, XCMPLX_1:6, XCMPLX_1:88;
then A119: ((((gg . I) `2 ) ^2 ) - 1) * ((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) = 0 ;
(((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 ) <> 0 by A116, COMPLEX1:2;
then A120: (((gg . I) `2 ) ^2 ) - 1 = 0 by A119, XCMPLX_1:6;
A121: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A122: sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

A123: now

assume A124: (gg . I) `2 = - 1 ; :: thesis: contradiction
then - (p4 `1 ) < 0 by A106, A111, A117, A100, A122, XREAL_1:143;
then - (- (p4 `1 )) > - 0 ;
hence contradiction by A105, A111, A117, A122, A124, EUCLID:56; :: thesis: verum

end;

A125: 1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ) > 0 by Lm1;
A126: ( (ff . O) `1 = (p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & (ff . O) `2 = (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A10, A3, A97, EUCLID:56;

A127: now

assume ( (ff . O) `1 = 0 & (ff . O) `2 = 0 ) ; :: thesis: contradiction
then ( p1 `1 = 0 & p1 `2 = 0 ) by A126, A121, XCMPLX_1:6;
hence contradiction by A96, 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 A5, A6, A121, XREAL_1:66;
then A128: ( ( p1 `2 <= p1 `1 & (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) or ( (ff . O) `2 >= (ff . O) `1 & (ff . O) `2 <= - ((ff . O) `1 ) ) ) by A126, A121, XREAL_1:66;
then ( ( (ff . O) `2 <= (ff . O) `1 & - ((ff . O) `1 ) <= (ff . O) `2 ) or ( (ff . O) `2 >= (ff . O) `1 & (ff . O) `2 <= - ((ff . O) `1 ) ) ) by A126, A121, XREAL_1:66;
then A129: Sq_Circ . (ff . O) = |[(((ff . O) `1 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )))),(((ff . O) `2 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))))]| by A127, Def1, JGRAPH_2:11;
A130: sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

A131: now

assume A132: (ff . O) `1 = 1 ; :: thesis: contradiction
- (p1 `2 ) >= - (- (p1 `1 )) by A6, XREAL_1:26;
then - (p1 `2 ) > 0 by A102, A129, A98, A130, A132, XREAL_1:141;
then - (- (p1 `2 )) < - 0 ;
hence contradiction by A5, A102, A129, A130, A132, EUCLID:56; :: thesis: verum

end;

consider p2 being Point of (TOP-REAL 2) such that
A133: f . I = p2 and
A134: |.p2.| = 1 and
A135: p2 `2 <= p2 `1 and
A136: p2 `2 >= - (p2 `1 ) by A2;
A137: ff . I = (Sq_Circ " ) . (f . I) by A9, FUNCT_1:22;
then A138: p2 = Sq_Circ . (ff . I) by A133, Th54, FUNCT_1:54;
A139: p2 <> 0. (TOP-REAL 2) by A134, TOPRNS_1:24;
then A140: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A135, A136, Th38;
then A141: (ff . I) `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A137, A133, EUCLID:56;
A142: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A143: (ff . I) `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A137, A133, A140, EUCLID:56;

A144: now

assume ( (ff . I) `1 = 0 & (ff . I) `2 = 0 ) ; :: thesis: contradiction
then ( p2 `1 = 0 & p2 `2 = 0 ) by A141, A143, A142, XCMPLX_1:6;
hence contradiction by A139, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A145: ( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( (ff . I) `2 >= (ff . I) `1 & (ff . I) `2 <= - ((ff . I) `1 ) ) ) by A135, A136, A142, XREAL_1:66;
then ( ( (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & - ((ff . I) `1 ) <= (ff . I) `2 ) or ( (ff . I) `2 >= (ff . I) `1 & (ff . I) `2 <= - ((ff . I) `1 ) ) ) by A137, A133, A140, A141, A142, EUCLID:56, XREAL_1:66;
then A146: Sq_Circ . (ff . I) = |[(((ff . I) `1 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )))),(((ff . I) `2 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))))]| by A141, A143, A144, Def1, JGRAPH_2:11;
A147: sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

A148: now

assume A149: (ff . I) `1 = - 1 ; :: thesis: contradiction
- (p2 `2 ) <= - (- (p2 `1 )) by A136, XREAL_1:26;
then - (p2 `2 ) < 0 by A138, A146, A99, A147, A149, XREAL_1:143;
then - (- (p2 `2 )) > - 0 ;
hence contradiction by A135, A138, A146, A147, A149, EUCLID:56; :: thesis: verum

end;

A150: 1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ) > 0 by Lm1;
|[(((ff . I) `1 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )))),(((ff . I) `2 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))))]| `2 = ((ff . I) `2 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) by EUCLID:56;
then |.p2.| ^2 = ((((ff . I) `1 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )))) ^2 ) + ((((ff . I) `2 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )))) ^2 ) by A138, A146, A99, JGRAPH_1:46
.= ((((ff . I) `1 ) ^2 ) / ((sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) ^2 )) + ((((ff . I) `2 ) / (sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((ff . I) `1 ) ^2 ) / ((sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) ^2 )) + ((((ff . I) `2 ) ^2 ) / ((sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((ff . I) `1 ) ^2 ) / (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) + ((((ff . I) `2 ) ^2 ) / ((sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) ^2 )) by A150, SQUARE_1:def 4
.= ((((ff . I) `1 ) ^2 ) / (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) + ((((ff . I) `2 ) ^2 ) / (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) by A150, SQUARE_1:def 4
.= ((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) / (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )) by XCMPLX_1:63 ;
then (((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) / (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ))) * (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )) = 1 * (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )) by A134;
then (((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 ) = 1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ) by A150, XCMPLX_1:88;
then A151: ((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) - 1 = (((ff . I) `2 ) ^2 ) / (((ff . I) `1 ) ^2 ) by XCMPLX_1:77;
(ff . I) `1 <> 0 by A141, A143, A142, A144, A145, XREAL_1:66;
then (((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) - 1) * (((ff . I) `1 ) ^2 ) = ((ff . I) `2 ) ^2 by A151, XCMPLX_1:6, XCMPLX_1:88;
then A152: ((((ff . I) `1 ) ^2 ) - 1) * ((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) = 0 ;
(((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 ) <> 0 by A144, COMPLEX1:2;
then A153: (((ff . I) `1 ) ^2 ) - 1 = 0 by A152, XCMPLX_1:6;
A154: |[(((gg . O) `1 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )))),(((gg . O) `2 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))))]| `2 = ((gg . O) `2 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) by EUCLID:56;
A155: 1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ) > 0 by Lm1;
|[(((ff . O) `1 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )))),(((ff . O) `2 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))))]| `2 = ((ff . O) `2 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) by EUCLID:56;
then |.p1.| ^2 = ((((ff . O) `1 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )))) ^2 ) + ((((ff . O) `2 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )))) ^2 ) by A102, A129, A98, JGRAPH_1:46
.= ((((ff . O) `1 ) ^2 ) / ((sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) ^2 )) + ((((ff . O) `2 ) / (sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((ff . O) `1 ) ^2 ) / ((sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) ^2 )) + ((((ff . O) `2 ) ^2 ) / ((sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((ff . O) `1 ) ^2 ) / (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) + ((((ff . O) `2 ) ^2 ) / ((sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) ^2 )) by A155, SQUARE_1:def 4
.= ((((ff . O) `1 ) ^2 ) / (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) + ((((ff . O) `2 ) ^2 ) / (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) by A155, SQUARE_1:def 4
.= ((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) / (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )) by XCMPLX_1:63 ;
then (((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) / (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ))) * (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )) = 1 * (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )) by A4;
then (((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 ) = 1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ) by A155, XCMPLX_1:88;
then A156: ((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) - 1 = (((ff . O) `2 ) ^2 ) / (((ff . O) `1 ) ^2 ) by XCMPLX_1:77;
(ff . O) `1 <> 0 by A126, A121, A127, A128, XREAL_1:66;
then (((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) - 1) * (((ff . O) `1 ) ^2 ) = ((ff . O) `2 ) ^2 by A156, XCMPLX_1:6, XCMPLX_1:88;
then A157: ((((ff . O) `1 ) ^2 ) - 1) * ((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) = 0 ;
consider p3 being Point of (TOP-REAL 2) such that
A158: g . O = p3 and
A159: |.p3.| = 1 and
A160: p3 `2 <= p3 `1 and
A161: p3 `2 <= - (p3 `1 ) by A2;
A162: p3 <> 0. (TOP-REAL 2) by A159, TOPRNS_1:24;
A163: gg . O = (Sq_Circ " ) . (g . O) by A8, FUNCT_1:22;
then A164: p3 = Sq_Circ . (gg . O) by A158, Th54, FUNCT_1:54;
A165: - (p3 `2 ) >= - (- (p3 `1 )) by A161, XREAL_1:26;
then A166: (Sq_Circ " ) . p3 = |[((p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A160, A162, Th40;
then A167: (gg . O) `2 = (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) by A163, A158, EUCLID:56;
A168: sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A169: (gg . O) `1 = (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) by A163, A158, A166, EUCLID:56;

A170: now

assume ( (gg . O) `2 = 0 & (gg . O) `1 = 0 ) ; :: thesis: contradiction
then ( p3 `2 = 0 & p3 `1 = 0 ) by A167, A169, A168, XCMPLX_1:6;
hence contradiction by A162, 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 A160, A165, A168, XREAL_1:66;
then A171: ( ( p3 `1 <= p3 `2 & (- (p3 `2 )) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) or ( (gg . O) `1 >= (gg . O) `2 & (gg . O) `1 <= - ((gg . O) `2 ) ) ) by A167, A169, A168, XREAL_1:66;
then ( ( (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) & - ((gg . O) `2 ) <= (gg . O) `1 ) or ( (gg . O) `1 >= (gg . O) `2 & (gg . O) `1 <= - ((gg . O) `2 ) ) ) by A163, A158, A166, A167, A168, EUCLID:56, XREAL_1:66;
then A172: Sq_Circ . (gg . O) = |[(((gg . O) `1 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )))),(((gg . O) `2 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))))]| by A167, A169, A170, Th14, JGRAPH_2:11;
A173: sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

A174: now

assume A175: (gg . O) `2 = 1 ; :: thesis: contradiction
then - (p3 `1 ) > 0 by A161, A164, A172, A154, A173, XREAL_1:141;
then - (- (p3 `1 )) < - 0 ;
hence contradiction by A160, A164, A172, A173, A175, EUCLID:56; :: thesis: verum

end;

|[(((gg . O) `1 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )))),(((gg . O) `2 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))))]| `1 = ((gg . O) `1 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) by EUCLID:56;
then |.p3.| ^2 = ((((gg . O) `2 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )))) ^2 ) + ((((gg . O) `1 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )))) ^2 ) by A164, A172, A154, JGRAPH_1:46
.= ((((gg . O) `2 ) ^2 ) / ((sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) ^2 )) + ((((gg . O) `1 ) / (sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= ((((gg . O) `2 ) ^2 ) / ((sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) ^2 )) + ((((gg . O) `1 ) ^2 ) / ((sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= ((((gg . O) `2 ) ^2 ) / (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) + ((((gg . O) `1 ) ^2 ) / ((sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) ^2 )) by A125, SQUARE_1:def 4
.= ((((gg . O) `2 ) ^2 ) / (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) + ((((gg . O) `1 ) ^2 ) / (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) by A125, SQUARE_1:def 4
.= ((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) / (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )) by XCMPLX_1:63 ;
then (((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) / (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ))) * (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )) = 1 * (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )) by A159;
then (((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 ) = 1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ) by A125, XCMPLX_1:88;
then A176: ((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) - 1 = (((gg . O) `1 ) ^2 ) / (((gg . O) `2 ) ^2 ) by XCMPLX_1:77;
(gg . O) `2 <> 0 by A167, A169, A168, A170, A171, XREAL_1:66;
then (((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) - 1) * (((gg . O) `2 ) ^2 ) = ((gg . O) `1 ) ^2 by A176, XCMPLX_1:6, XCMPLX_1:88;
then A177: ((((gg . O) `2 ) ^2 ) - 1) * ((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) = 0 ;
(((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 ) <> 0 by A170, COMPLEX1:2;
then A178: (((gg . O) `2 ) ^2 ) - 1 = 0 by A177, XCMPLX_1:6;
(((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 ) <> 0 by A127, COMPLEX1:2;
then (((ff . O) `1 ) ^2 ) - 1 = 0 by A157, XCMPLX_1:6;
hence ( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 ) by A131, A153, A148, A178, A174, A120, A123, Lm20; :: thesis: verum

end;

then rng ff meets rng gg by A2, A12, Th52, JGRAPH_1:65;
then A179: (rng ff) /\ (rng gg) <> {} by XBOOLE_0:def 7;
then y in rng ff by XBOOLE_0:def 4;
then consider x1 being set such that
A180: x1 in dom ff and
A181: y = ff . x1 by FUNCT_1:def 5;
x1 in dom f by A180, FUNCT_1:21;
then A182: f . x1 in rng f by FUNCT_1:def 5;
y in rng gg by A179, XBOOLE_0:def 4;
then consider x2 being set such that
A183: x2 in dom gg and
A184: y = gg . x2 by FUNCT_1:def 5;
A185: gg . x2 = (Sq_Circ " ) . (g . x2) by A183, FUNCT_1:22;
x2 in dom g by A183, FUNCT_1:21;
then A186: g . x2 in rng g by FUNCT_1:def 5;
ff . x1 = (Sq_Circ " ) . (f . x1) by A180, FUNCT_1:22;
then f . x1 = g . x2 by A181, A184, A1, A182, A186, A185, FUNCT_1:def 8;
then (rng f) /\ (rng g) <> {} by A182, A186, XBOOLE_0:def 4;
hence rng f meets rng g by XBOOLE_0:def 7; :: thesis: verum