A1: dom (Sq_Circ ") = the carrier of (TOP-REAL 2) by Th29, 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 Th29, FUNCT_2:13;
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 Th29, FUNCT_2:13;
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:12;
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:3;
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:3;
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:12;

A18: now :: thesis: ( ( p2 = 0. (TOP-REAL 2) & - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) 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 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (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 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (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: ( - 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, Th28, JGRAPH_2:3; :: 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, Th28;
then A21: (gg . r) `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A17, A15, EUCLID:52;
|.p2.| ^2 <= |.p2.| by A16, SQUARE_1:42;
then A22: |.p2.| ^2 <= 1 by A16, XXREAL_0:2;
A23: ((gg . r) `2) ^2 >= 0 by XREAL_1:63;
A24: ((gg . r) `1) ^2 >= 0 by XREAL_1:63;
A25: (gg . r) `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A17, A15, A20, EUCLID:52;
A26: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by Lm1, SQUARE_1:25;
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:64;
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:64;
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:52, XREAL_1:64;

A29: now :: thesis: ( (gg . r) `1 = 0 implies not (gg . r) `2 = 0 )

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:53, EUCLID:54; :: thesis: verum

end;

then A30: (gg . r) `1 <> 0 by A21, A25, A26, A27, XREAL_1:64;
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:52;
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, Th43, EUCLID:52, FUNCT_1:32;
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:3;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((gg . r) `1) ^2) + (((gg . r) `2) ^2)) / (1 + ((((gg . r) `2) / ((gg . r) `1)) ^2)) by XCMPLX_1:62 ;
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:64;
then (((gg . r) `1) ^2) + (((gg . r) `2) ^2) <= 1 + ((((gg . r) `2) / ((gg . r) `1)) ^2) by A32, XCMPLX_1:87;
then (((gg . r) `1) ^2) + (((gg . r) `2) ^2) <= 1 + ((((gg . r) `2) ^2) / (((gg . r) `1) ^2)) by XCMPLX_1:76;
then ((((gg . r) `1) ^2) + (((gg . r) `2) ^2)) - 1 <= (((gg . r) `2) ^2) / (((gg . r) `1) ^2) by XREAL_1:20;
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:64;
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:87;
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:1;
then A35: (((gg . r) `1) ^2) - 1 <= 0 by A24, A34, A23, XREAL_1:129;
then A36: (gg . r) `1 >= - 1 by SQUARE_1:43;
A37: (gg . r) `1 <= 1 by A35, SQUARE_1:43;
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:24, 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:24;
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:24, XXREAL_0:2;
hence ( - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) by A35, SQUARE_1:43, XREAL_1:24; :: 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, Th28;
then A40: (gg . r) `2 = (p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by A17, A15, EUCLID:52;
A41: (gg . r) `1 = (p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by A17, A15, A39, EUCLID:52;
A42: sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ) by A38, 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 A42, XREAL_1:64;
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:64;
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:52, XREAL_1:64;

A45: now :: thesis: ( (gg . r) `2 = 0 implies not (gg . r) `1 = 0 )

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:64;
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, Th43, EUCLID:52, FUNCT_1:32;
A49: ((gg . r) `2) ^2 >= 0 by XREAL_1:63;
|.p2.| ^2 <= |.p2.| by A16, SQUARE_1:42;
then A50: |.p2.| ^2 <= 1 by A16, XXREAL_0:2;
A51: ((gg . r) `1) ^2 >= 0 by XREAL_1:63;
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:52;
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, Th4, JGRAPH_2:3;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((gg . r) `2) ^2) + (((gg . r) `1) ^2)) / (1 + ((((gg . r) `1) / ((gg . r) `2)) ^2)) by XCMPLX_1:62 ;
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:64;
then (((gg . r) `2) ^2) + (((gg . r) `1) ^2) <= 1 + ((((gg . r) `1) / ((gg . r) `2)) ^2) by A53, XCMPLX_1:87;
then (((gg . r) `2) ^2) + (((gg . r) `1) ^2) <= 1 + ((((gg . r) `1) ^2) / (((gg . r) `2) ^2)) by XCMPLX_1:76;
then ((((gg . r) `2) ^2) + (((gg . r) `1) ^2)) - 1 <= (((gg . r) `1) ^2) / (((gg . r) `2) ^2) by XREAL_1:20;
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:64;
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:87;
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:1;
then A55: (((gg . r) `2) ^2) - 1 <= 0 by A49, A54, A51, XREAL_1:129;
then A56: (gg . r) `2 >= - 1 by SQUARE_1:43;
A57: (gg . r) `2 <= 1 by A55, SQUARE_1:43;
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:24, 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:24, 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:24;
hence ( - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) by A55, SQUARE_1:43; :: thesis: verum

end;

end;

end;

A58: ff . r = (Sq_Circ ") . (f . r) by A9, FUNCT_1:12;

now :: thesis: ( ( p1 = 0. (TOP-REAL 2) & - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 ) 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 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (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 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (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: ( - 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, Th28, JGRAPH_2:3; :: 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, Th28;
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:52;
A61: sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) > 0 by Lm1, SQUARE_1:25;
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:64;
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:64;
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:64;

A64: now :: thesis: ( (ff . r) `1 = 0 implies not (ff . r) `2 = 0 )

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:53, EUCLID:54; :: thesis: verum

end;

then A65: (ff . r) `1 <> 0 by A60, A61, A62, XREAL_1:64;
|.p1.| ^2 <= |.p1.| by A14, SQUARE_1:42;
then A66: |.p1.| ^2 <= 1 by A14, XXREAL_0:2;
A67: ((ff . r) `1) ^2 >= 0 by XREAL_1:63;
A68: ((ff . r) `2) ^2 >= 0 by XREAL_1:63;
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:52;
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, Th43, EUCLID:52, FUNCT_1:32;
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:3;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((ff . r) `1) ^2) + (((ff . r) `2) ^2)) / (1 + ((((ff . r) `2) / ((ff . r) `1)) ^2)) by XCMPLX_1:62 ;
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:64;
then (((ff . r) `1) ^2) + (((ff . r) `2) ^2) <= 1 + ((((ff . r) `2) / ((ff . r) `1)) ^2) by A70, XCMPLX_1:87;
then (((ff . r) `1) ^2) + (((ff . r) `2) ^2) <= 1 + ((((ff . r) `2) ^2) / (((ff . r) `1) ^2)) by XCMPLX_1:76;
then ((((ff . r) `1) ^2) + (((ff . r) `2) ^2)) - 1 <= (((ff . r) `2) ^2) / (((ff . r) `1) ^2) by XREAL_1:20;
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:64;
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:87;
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:1;
then A73: (((ff . r) `1) ^2) - 1 <= 0 by A67, A72, A68, XREAL_1:129;
then A74: (ff . r) `1 >= - 1 by SQUARE_1:43;
A75: (ff . r) `1 <= 1 by A73, SQUARE_1:43;
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:24, 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:24;
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:24, XXREAL_0:2;
hence ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 ) by A73, SQUARE_1:43, XREAL_1:24; :: 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, Th28;
then A78: (ff . r) `2 = (p1 `2) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))) by A58, A13, EUCLID:52;
A79: (ff . r) `1 = (p1 `1) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))) by A58, A13, A77, EUCLID:52;
A80: sqrt (1 + (((p1 `1) / (p1 `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
( ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) ) ) by A76, 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 A80, XREAL_1:64;
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:64;
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:52, XREAL_1:64;

A83: now :: thesis: ( (ff . r) `2 = 0 implies not (ff . r) `1 = 0 )

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:64;
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, Th43, EUCLID:52, FUNCT_1:32;
A87: ((ff . r) `2) ^2 >= 0 by XREAL_1:63;
|.p1.| ^2 <= |.p1.| by A14, SQUARE_1:42;
then A88: |.p1.| ^2 <= 1 by A14, XXREAL_0:2;
A89: ((ff . r) `1) ^2 >= 0 by XREAL_1:63;
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:52;
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, Th4, JGRAPH_2:3;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((ff . r) `2) ^2) + (((ff . r) `1) ^2)) / (1 + ((((ff . r) `1) / ((ff . r) `2)) ^2)) by XCMPLX_1:62 ;
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:64;
then (((ff . r) `2) ^2) + (((ff . r) `1) ^2) <= 1 + ((((ff . r) `1) / ((ff . r) `2)) ^2) by A91, XCMPLX_1:87;
then (((ff . r) `2) ^2) + (((ff . r) `1) ^2) <= 1 + ((((ff . r) `1) ^2) / (((ff . r) `2) ^2)) by XCMPLX_1:76;
then ((((ff . r) `2) ^2) + (((ff . r) `1) ^2)) - 1 <= (((ff . r) `1) ^2) / (((ff . r) `2) ^2) by XREAL_1:20;
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:64;
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:87;
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:1;
then A93: (((ff . r) `2) ^2) - 1 <= 0 by A87, A92, A89, XREAL_1:129;
then A94: (ff . r) `2 >= - 1 by SQUARE_1:43;
A95: (ff . r) `2 <= 1 by A93, SQUARE_1:43;
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:24, 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:24, 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:24;
hence ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 ) by A93, SQUARE_1:43; :: 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;

set y = the Element of (rng ff) /\ (rng gg);
A96: p1 <> 0. (TOP-REAL 2) by A4, TOPRNS_1:23;
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, Th28;
( (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:52;
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:52;
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:52;
A101: 1 + ((((gg . I) `1) / ((gg . I) `2)) ^2) > 0 by Lm1;
(Sq_Circ ") . p1 = ff . O by A9, A3, FUNCT_1:12;
then A102: p1 = Sq_Circ . (ff . O) by Th43, FUNCT_1:32;
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:25;
A108: - (p4 `2) <= - (- (p4 `1)) by A106, XREAL_1:24;
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:64;
A110: gg . I = (Sq_Circ ") . (g . I) by A8, FUNCT_1:12;
then A111: p4 = Sq_Circ . (gg . I) by A103, Th43, FUNCT_1:32;
A112: p4 <> 0. (TOP-REAL 2) by A104, TOPRNS_1:23;
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, Th30;
then A114: (gg . I) `2 = (p4 `2) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))) by A110, A103, EUCLID:52;
A115: (gg . I) `1 = (p4 `1) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))) by A110, A103, A113, EUCLID:52;

A116: now :: thesis: ( (gg . I) `2 = 0 implies not (gg . I) `1 = 0 )

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:53, EUCLID:54; :: 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:52, XREAL_1:64;
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, Th4, JGRAPH_2:3;
|[(((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:52;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((gg . I) `2) ^2) + (((gg . I) `1) ^2)) / (1 + ((((gg . I) `1) / ((gg . I) `2)) ^2)) by XCMPLX_1:62 ;
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:87;
then A118: ((((gg . I) `2) ^2) + (((gg . I) `1) ^2)) - 1 = (((gg . I) `1) ^2) / (((gg . I) `2) ^2) by XCMPLX_1:76;
(gg . I) `2 <> 0 by A114, A115, A107, A116, A109, XREAL_1:64;
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:87;
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:1;
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:25;
A122: sqrt (1 + ((((gg . I) `1) / ((gg . I) `2)) ^2)) > 0 by Lm1, SQUARE_1:25;

A123: now :: thesis: not (gg . I) `2 = - 1

assume A124: (gg . I) `2 = - 1 ; :: thesis: contradiction
then - (p4 `1) < 0 by A106, A111, A117, A100, A122, XREAL_1:141;
then - (- (p4 `1)) > - 0 ;
hence contradiction by A105, A111, A117, A122, A124, EUCLID:52; :: 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:52;

A127: now :: thesis: ( (ff . O) `1 = 0 implies not (ff . O) `2 = 0 )

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: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 A5, A6, A121, XREAL_1:64;
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:64;
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:64;
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:3;
A130: sqrt (1 + ((((ff . O) `2) / ((ff . O) `1)) ^2)) > 0 by Lm1, SQUARE_1:25;

A131: now :: thesis: not (ff . O) `1 = 1

assume A132: (ff . O) `1 = 1 ; :: thesis: contradiction
- (p1 `2) >= - (- (p1 `1)) by A6, XREAL_1:24;
then - (p1 `2) > 0 by A102, A129, A98, A130, A132, XREAL_1:139;
then - (- (p1 `2)) < - 0 ;
hence contradiction by A5, A102, A129, A130, A132, EUCLID:52; :: 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:12;
then A138: p2 = Sq_Circ . (ff . I) by A133, Th43, FUNCT_1:32;
A139: p2 <> 0. (TOP-REAL 2) by A134, TOPRNS_1:23;
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, Th28;
then A141: (ff . I) `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A137, A133, EUCLID:52;
A142: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by Lm1, SQUARE_1:25;
A143: (ff . I) `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A137, A133, A140, EUCLID:52;

A144: now :: thesis: ( (ff . I) `1 = 0 implies not (ff . I) `2 = 0 )

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:53, EUCLID:54; :: 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:64;
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:52, XREAL_1:64;
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:3;
A147: sqrt (1 + ((((ff . I) `2) / ((ff . I) `1)) ^2)) > 0 by Lm1, SQUARE_1:25;

A148: now :: thesis: not (ff . I) `1 = - 1

assume A149: (ff . I) `1 = - 1 ; :: thesis: contradiction
- (p2 `2) <= - (- (p2 `1)) by A136, XREAL_1:24;
then - (p2 `2) < 0 by A138, A146, A99, A147, A149, XREAL_1:141;
then - (- (p2 `2)) > - 0 ;
hence contradiction by A135, A138, A146, A147, A149, EUCLID:52; :: 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:52;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((ff . I) `1) ^2) + (((ff . I) `2) ^2)) / (1 + ((((ff . I) `2) / ((ff . I) `1)) ^2)) by XCMPLX_1:62 ;
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:87;
then A151: ((((ff . I) `1) ^2) + (((ff . I) `2) ^2)) - 1 = (((ff . I) `2) ^2) / (((ff . I) `1) ^2) by XCMPLX_1:76;
(ff . I) `1 <> 0 by A141, A143, A142, A144, A145, XREAL_1:64;
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:87;
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:1;
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:52;
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:52;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((ff . O) `1) ^2) + (((ff . O) `2) ^2)) / (1 + ((((ff . O) `2) / ((ff . O) `1)) ^2)) by XCMPLX_1:62 ;
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:87;
then A156: ((((ff . O) `1) ^2) + (((ff . O) `2) ^2)) - 1 = (((ff . O) `2) ^2) / (((ff . O) `1) ^2) by XCMPLX_1:76;
(ff . O) `1 <> 0 by A126, A121, A127, A128, XREAL_1:64;
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:87;
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:23;
A163: gg . O = (Sq_Circ ") . (g . O) by A8, FUNCT_1:12;
then A164: p3 = Sq_Circ . (gg . O) by A158, Th43, FUNCT_1:32;
A165: - (p3 `2) >= - (- (p3 `1)) by A161, XREAL_1:24;
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, Th30;
then A167: (gg . O) `2 = (p3 `2) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))) by A163, A158, EUCLID:52;
A168: sqrt (1 + (((p3 `1) / (p3 `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
A169: (gg . O) `1 = (p3 `1) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))) by A163, A158, A166, EUCLID:52;

A170: now :: thesis: ( (gg . O) `2 = 0 implies not (gg . O) `1 = 0 )

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: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 A160, A165, A168, XREAL_1:64;
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:64;
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:52, XREAL_1:64;
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, Th4, JGRAPH_2:3;
A173: sqrt (1 + ((((gg . O) `1) / ((gg . O) `2)) ^2)) > 0 by Lm1, SQUARE_1:25;

A174: now :: thesis: not (gg . O) `2 = 1

assume A175: (gg . O) `2 = 1 ; :: thesis: contradiction
then - (p3 `1) > 0 by A161, A164, A172, A154, A173, XREAL_1:139;
then - (- (p3 `1)) < - 0 ;
hence contradiction by A160, A164, A172, A173, A175, EUCLID:52; :: 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:52;
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:29
.= ((((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:76
.= ((((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:76
.= ((((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 2
.= ((((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 2
.= ((((gg . O) `2) ^2) + (((gg . O) `1) ^2)) / (1 + ((((gg . O) `1) / ((gg . O) `2)) ^2)) by XCMPLX_1:62 ;
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:87;
then A176: ((((gg . O) `2) ^2) + (((gg . O) `1) ^2)) - 1 = (((gg . O) `1) ^2) / (((gg . O) `2) ^2) by XCMPLX_1:76;
(gg . O) `2 <> 0 by A167, A169, A168, A170, A171, XREAL_1:64;
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:87;
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:1;
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:1;
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, Th42, JGRAPH_1:47;
then A179: (rng ff) /\ (rng gg) <> {} ;
then the Element of (rng ff) /\ (rng gg) in rng ff by XBOOLE_0:def 4;
then consider x1 being object such that
A180: x1 in dom ff and
A181: the Element of (rng ff) /\ (rng gg) = ff . x1 by FUNCT_1:def 3;
x1 in dom f by A180, FUNCT_1:11;
then A182: f . x1 in rng f by FUNCT_1:def 3;
the Element of (rng ff) /\ (rng gg) in rng gg by A179, XBOOLE_0:def 4;
then consider x2 being object such that
A183: x2 in dom gg and
A184: the Element of (rng ff) /\ (rng gg) = gg . x2 by FUNCT_1:def 3;
A185: gg . x2 = (Sq_Circ ") . (g . x2) by A183, FUNCT_1:12;
x2 in dom g by A183, FUNCT_1:11;
then A186: g . x2 in rng g by FUNCT_1:def 3;
ff . x1 = (Sq_Circ ") . (f . x1) by A180, FUNCT_1:12;
then f . x1 = g . x2 by A181, A184, A1, A182, A186, A185, FUNCT_1:def 4;
then (rng f) /\ (rng g) <> {} by A182, A186, XBOOLE_0:def 4;
hence rng f meets rng g ; :: thesis: verum