let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let C0, KXP, KXN, KYP, KYN be Subset of (TOP-REAL 2); :: thesis: for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let O, I be Point of I[01] ; :: thesis: ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 implies rng f meets rng g )
assume A1: ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 ) ; :: thesis: rng f meets rng g
reconsider ff = (Sq_Circ " ) * f as Function of I[01] ,(TOP-REAL 2) by Th39, FUNCT_2:19;
reconsider gg = (Sq_Circ " ) * g as Function of I[01] ,(TOP-REAL 2) by Th39, FUNCT_2:19;
consider h1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A2: ( h1 = Sq_Circ " & h1 is continuous ) by Th52;
A3: dom ff = the carrier of I[01] by FUNCT_2:def 1;
A4: dom gg = the carrier of I[01] by FUNCT_2:def 1;
A5: dom f = the carrier of I[01] by FUNCT_2:def 1;
A6: dom g = the carrier of I[01] by FUNCT_2:def 1;
A7: ff is continuous by A1, A2;
A9: gg is continuous by A1, A2;
A11: ff . O = (Sq_Circ " ) . (f . O) by A3, FUNCT_1:22;
consider p1 being Point of (TOP-REAL 2) such that
A12: ( f . O = p1 & |.p1.| = 1 & p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) by A1;
A13: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) by A12, TOPRNS_1:24;
then A14: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by Th38;
A15: ( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 )
proof
set px = ff . O;
set q = ff . O;
A16: (Sq_Circ " ) . p1 = ff . O by A3, A12, FUNCT_1:22;
A17: ( (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 A11, A12, A14, EUCLID:56;
A18: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A19: now
assume A20: ( (ff . O) `1 = 0 & (ff . O) `2 = 0 ) ; :: thesis: contradiction
then A21: p1 `1 = 0 by A17, A18, XCMPLX_1:6;
p1 `2 = 0 by A17, A18, A20, XCMPLX_1:6;
hence contradiction by A13, A21, EUCLID:57, EUCLID:58; :: thesis: verum
end;
( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) ) by A12, A18, XREAL_1:66;
then A22: ( ( p1 `2 <= p1 `1 & (- (p1 `1 )) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) <= (p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) or ( (ff . O) `2 >= (ff . O) `1 & (ff . O) `2 <= - ((ff . O) `1 ) ) ) by A17, A18, XREAL_1:66;
then A23: ( ( (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 A17, A18, XREAL_1:66;
A24: p1 = Sq_Circ . (ff . O) by A16, Th54, FUNCT_1:54;
A25: 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 A19, A23, Def1, JGRAPH_2:11;
A26: ( |[(((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 ))) & |[(((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;
A27: 1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ) > 0 by Lm1;
A28: sqrt (1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A29: (ff . O) `1 <> 0 by A17, A18, A19, A22, XREAL_1:66;
|.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 A24, A25, A26, 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 A27, 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 A27, 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 A12;
then (((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 ) = 1 + ((((ff . O) `2 ) / ((ff . O) `1 )) ^2 ) by A27, XCMPLX_1:88;
then ((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) - 1 = (((ff . O) `2 ) ^2 ) / (((ff . O) `1 ) ^2 ) by XCMPLX_1:77;
then (((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) - 1) * (((ff . O) `1 ) ^2 ) = ((ff . O) `2 ) ^2 by A29, XCMPLX_1:6, XCMPLX_1:88;
then A30: ((((ff . O) `1 ) ^2 ) - 1) * ((((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 )) = 0 ;
(((ff . O) `1 ) ^2 ) + (((ff . O) `2 ) ^2 ) <> 0 by A19, COMPLEX1:2;
then A31: (((ff . O) `1 ) ^2 ) - 1 = 0 by A30, XCMPLX_1:6;
A32: now
assume A33: (ff . O) `1 = 1 ; :: thesis: contradiction
- (p1 `2 ) >= - (- (p1 `1 )) by A12, XREAL_1:26;
then - (p1 `2 ) > 0 by A24, A25, A26, A28, A33, XREAL_1:141;
then - (- (p1 `2 )) < - 0 ;
hence contradiction by A12, A24, A25, A26, A28, A33; :: thesis: verum
end;
A34: ff . I = (Sq_Circ " ) . (f . I) by A3, FUNCT_1:22;
consider p2 being Point of (TOP-REAL 2) such that
A35: ( f . I = p2 & |.p2.| = 1 & p2 `2 <= p2 `1 & p2 `2 >= - (p2 `1 ) ) by A1;
A36: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) by A35, TOPRNS_1:24;
then A37: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by Th38;
set py = ff . I;
A38: ( (ff . I) `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & (ff . I) `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) by A34, A35, A37, EUCLID:56;
A39: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A40: now
assume A41: ( (ff . I) `1 = 0 & (ff . I) `2 = 0 ) ; :: thesis: contradiction
then A42: p2 `1 = 0 by A38, A39, XCMPLX_1:6;
p2 `2 = 0 by A38, A39, A41, XCMPLX_1:6;
hence contradiction by A36, A42, EUCLID:57, EUCLID:58; :: thesis: verum
end;
A43: now
( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( (ff . I) `2 >= (ff . I) `1 & (ff . I) `2 <= - ((ff . I) `1 ) ) ) by A35, A39, XREAL_1:66;
hence ( ( (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & - ((ff . I) `1 ) <= (ff . I) `2 ) or ( (ff . I) `2 >= (ff . I) `1 & (ff . I) `2 <= - ((ff . I) `1 ) ) ) by A38, A39, XREAL_1:66; :: thesis: verum
end;
A44: p2 = Sq_Circ . (ff . I) by A34, A35, Th54, FUNCT_1:54;
A45: 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 A38, A40, A43, Def1, JGRAPH_2:11;
A46: ( |[(((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 ))) & |[(((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;
A47: 1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ) > 0 by Lm1;
A48: sqrt (1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A49: (ff . I) `1 <> 0 by A38, A40, A43;
|.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 A44, A45, A46, 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 A47, 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 A47, 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 A35;
then (((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 ) = 1 + ((((ff . I) `2 ) / ((ff . I) `1 )) ^2 ) by A47, XCMPLX_1:88;
then ((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) - 1 = (((ff . I) `2 ) ^2 ) / (((ff . I) `1 ) ^2 ) by XCMPLX_1:77;
then (((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) - 1) * (((ff . I) `1 ) ^2 ) = ((ff . I) `2 ) ^2 by A49, XCMPLX_1:6, XCMPLX_1:88;
then A50: ((((ff . I) `1 ) ^2 ) - 1) * ((((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 )) = 0 ;
(((ff . I) `1 ) ^2 ) + (((ff . I) `2 ) ^2 ) <> 0 by A40, COMPLEX1:2;
then A51: (((ff . I) `1 ) ^2 ) - 1 = 0 by A50, XCMPLX_1:6;
A52: now
assume A53: (ff . I) `1 = - 1 ; :: thesis: contradiction
- (p2 `2 ) <= - (- (p2 `1 )) by A35, XREAL_1:26;
then - (p2 `2 ) < 0 by A44, A45, A46, A48, A53, XREAL_1:143;
then - (- (p2 `2 )) > - 0 ;
hence contradiction by A35, A44, A45, A46, A48, A53; :: thesis: verum
end;
A54: gg . O = (Sq_Circ " ) . (g . O) by A4, FUNCT_1:22;
consider p3 being Point of (TOP-REAL 2) such that
A55: ( g . O = p3 & |.p3.| = 1 & p3 `2 <= p3 `1 & p3 `2 <= - (p3 `1 ) ) by A1;
A56: - (p3 `2 ) >= - (- (p3 `1 )) by A55, XREAL_1:26;
then A57: ( p3 <> 0. (TOP-REAL 2) & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) ) by A55, TOPRNS_1:24;
then A58: (Sq_Circ " ) . p3 = |[((p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by Th40;
set pz = gg . O;
A59: ( (gg . O) `2 = (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) & (gg . O) `1 = (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) by A54, A55, A58, EUCLID:56;
A60: sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A61: now
assume A62: ( (gg . O) `2 = 0 & (gg . O) `1 = 0 ) ; :: thesis: contradiction
then A63: p3 `2 = 0 by A59, A60, XCMPLX_1:6;
p3 `1 = 0 by A59, A60, A62, XCMPLX_1:6;
hence contradiction by A57, A63, EUCLID:57, EUCLID:58; :: thesis: verum
end;
A64: now
( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (- (p3 `2 )) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) ) by A55, A56, A60, XREAL_1:66;
then ( ( p3 `1 <= p3 `2 & (- (p3 `2 )) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) ) or ( (gg . O) `1 >= (gg . O) `2 & (gg . O) `1 <= - ((gg . O) `2 ) ) ) by A59, A60, XREAL_1:66;
hence ( ( (p3 `1 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) <= (p3 `2 ) * (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))) & - ((gg . O) `2 ) <= (gg . O) `1 ) or ( (gg . O) `1 >= (gg . O) `2 & (gg . O) `1 <= - ((gg . O) `2 ) ) ) by A59, A60, XREAL_1:66; :: thesis: verum
end;
A65: p3 = Sq_Circ . (gg . O) by A54, A55, Th54, FUNCT_1:54;
A66: 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 A59, A61, A64, Th14, JGRAPH_2:11;
A67: ( |[(((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 ))) & |[(((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;
A68: 1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ) > 0 by Lm1;
A69: sqrt (1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A70: (gg . O) `2 <> 0 by A59, A61, A64;
|.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 A65, A66, A67, 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 A68, 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 A68, 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 A55;
then (((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 ) = 1 + ((((gg . O) `1 ) / ((gg . O) `2 )) ^2 ) by A68, XCMPLX_1:88;
then ((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) - 1 = (((gg . O) `1 ) ^2 ) / (((gg . O) `2 ) ^2 ) by XCMPLX_1:77;
then (((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) - 1) * (((gg . O) `2 ) ^2 ) = ((gg . O) `1 ) ^2 by A70, XCMPLX_1:6, XCMPLX_1:88;
then A71: ((((gg . O) `2 ) ^2 ) - 1) * ((((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 )) = 0 ;
(((gg . O) `2 ) ^2 ) + (((gg . O) `1 ) ^2 ) <> 0 by A61, COMPLEX1:2;
then A72: (((gg . O) `2 ) ^2 ) - 1 = 0 by A71, XCMPLX_1:6;
A73: now
assume A74: (gg . O) `2 = 1 ; :: thesis: contradiction
then - (p3 `1 ) > 0 by A55, A65, A66, A67, A69, XREAL_1:141;
then - (- (p3 `1 )) < - 0 ;
hence contradiction by A55, A65, A66, A67, A69, A74; :: thesis: verum
end;
A75: gg . I = (Sq_Circ " ) . (g . I) by A4, FUNCT_1:22;
consider p4 being Point of (TOP-REAL 2) such that
A76: ( g . I = p4 & |.p4.| = 1 & p4 `2 >= p4 `1 & p4 `2 >= - (p4 `1 ) ) by A1;
A77: - (p4 `2 ) <= - (- (p4 `1 )) by A76, XREAL_1:26;
then A78: ( p4 <> 0. (TOP-REAL 2) & ( ( p4 `1 <= p4 `2 & - (p4 `2 ) <= p4 `1 ) or ( p4 `1 >= p4 `2 & p4 `1 <= - (p4 `2 ) ) ) ) by A76, TOPRNS_1:24;
then A79: (Sq_Circ " ) . p4 = |[((p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )))),((p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))))]| by Th40;
set pu = gg . I;
A80: ( (gg . I) `2 = (p4 `2 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) & (gg . I) `1 = (p4 `1 ) * (sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 ))) ) by A75, A76, A79, EUCLID:56;
A81: sqrt (1 + (((p4 `1 ) / (p4 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A82: now
assume A83: ( (gg . I) `2 = 0 & (gg . I) `1 = 0 ) ; :: thesis: contradiction
then A84: p4 `2 = 0 by A80, A81, XCMPLX_1:6;
p4 `1 = 0 by A80, A81, A83, XCMPLX_1:6;
hence contradiction by A78, A84, EUCLID:57, EUCLID:58; :: thesis: verum
end;
A85: now
( ( 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 A76, A77, A81, XREAL_1:66;
hence ( ( (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 A80, A81, XREAL_1:66; :: thesis: verum
end;
A86: p4 = Sq_Circ . (gg . I) by A75, A76, Th54, FUNCT_1:54;
A87: 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 A80, A82, A85, Th14, JGRAPH_2:11;
A88: ( |[(((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 ))) & |[(((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;
A89: 1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ) > 0 by Lm1;
A90: sqrt (1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A91: (gg . I) `2 <> 0 by A80, A82, A85;
|.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 A86, A87, A88, 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 A89, 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 A89, 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 A76;
then (((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 ) = 1 + ((((gg . I) `1 ) / ((gg . I) `2 )) ^2 ) by A89, XCMPLX_1:88;
then ((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) - 1 = (((gg . I) `1 ) ^2 ) / (((gg . I) `2 ) ^2 ) by XCMPLX_1:77;
then (((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) - 1) * (((gg . I) `2 ) ^2 ) = ((gg . I) `1 ) ^2 by A91, XCMPLX_1:6, XCMPLX_1:88;
then A92: ((((gg . I) `2 ) ^2 ) - 1) * ((((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 )) = 0 ;
(((gg . I) `2 ) ^2 ) + (((gg . I) `1 ) ^2 ) <> 0 by A82, COMPLEX1:2;
then A93: (((gg . I) `2 ) ^2 ) - 1 = 0 by A92, XCMPLX_1:6;
now
assume A94: (gg . I) `2 = - 1 ; :: thesis: contradiction
then - (p4 `1 ) < 0 by A76, A86, A87, A88, A90, XREAL_1:143;
then - (- (p4 `1 )) > - 0 ;
hence contradiction by A76, A86, A87, A88, A90, A94; :: thesis: verum
end;
hence ( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 ) by A31, A32, A51, A52, A72, A73, A93, Lm15; :: thesis: verum
end;
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 )
A95: ff . r = (Sq_Circ " ) . (f . r) by A3, FUNCT_1:22;
f . r in rng f by A5, FUNCT_1:12;
then f . r in C0 by A1;
then consider p1 being Point of (TOP-REAL 2) such that
A96: ( f . r = p1 & |.p1.| <= 1 ) by A1;
A97: 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 A95, A96, Th38, JGRAPH_2:11; :: thesis: verum
end;
case A98: ( 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 )
then A99: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by Th38;
set px = ff . r;
set q = ff . r;
A100: ( (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 A95, A96, A99, EUCLID:56;
A101: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
( ( 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 A98, A101, XREAL_1:66;
then A105: ( ( 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 A100, A101, XREAL_1:66;
then A106: ( ( (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 A100, A101, XREAL_1:66;
A107: p1 = Sq_Circ . (ff . r) by A95, A96, Th54, FUNCT_1:54;
A108: 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 A102, A106, Def1, JGRAPH_2:11;
A109: ( |[(((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 ))) & |[(((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;
A110: ((ff . r) `1 ) ^2 >= 0 by XREAL_1:65;
A111: 1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ) > 0 by Lm1;
|.p1.| ^2 <= |.p1.| by A96, SQUARE_1:111;
then A112: |.p1.| ^2 <= 1 by A96, XXREAL_0:2;
A113: (ff . r) `1 <> 0 by A100, A101, A102, A105, XREAL_1:66;
|.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 A107, A108, A109, 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 A111, 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 A111, 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 A111, A112, XREAL_1:66;
then (((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 ) <= 1 + ((((ff . r) `2 ) / ((ff . r) `1 )) ^2 ) by A111, 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 A110, XREAL_1:66;
then (((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) - 1) * (((ff . r) `1 ) ^2 ) <= ((ff . r) `2 ) ^2 by A113, XCMPLX_1:6, XCMPLX_1:88;
then A114: ((((ff . r) `1 ) ^2 ) - 1) * ((((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 )) <= 0 by Lm14;
A115: (((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 ) <> 0 by A102, COMPLEX1:2;
((ff . r) `2 ) ^2 >= 0 by XREAL_1:65;
then (((ff . r) `1 ) ^2 ) + (((ff . r) `2 ) ^2 ) >= 0 + 0 by A110;
then A116: (((ff . r) `1 ) ^2 ) - 1 <= 0 by A114, A115, XREAL_1:131;
then A117: ( (ff . r) `1 <= 1 & (ff . r) `1 >= - 1 ) by SQUARE_1:112;
now
( ( (ff . r) `2 <= 1 & - (- ((ff . r) `1 )) >= - ((ff . r) `2 ) ) or ( (ff . r) `2 >= - 1 & (ff . r) `2 <= - ((ff . r) `1 ) ) ) by A106, A117, 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 A117, XXREAL_0:2;
then ( ( (ff . r) `2 <= 1 & - 1 <= - (- ((ff . r) `2 )) ) or ( (ff . r) `2 >= - 1 & - ((ff . r) `2 ) >= - 1 ) ) by A117, XREAL_1:26, XXREAL_0:2;
hence ( ( (ff . r) `2 <= 1 & - 1 <= (ff . r) `2 ) or ( (ff . r) `2 >= - 1 & (ff . r) `2 <= 1 ) ) by XREAL_1:26; :: thesis: verum
end;
hence ( - 1 <= (ff . r) `1 & (ff . r) `1 <= 1 & - 1 <= (ff . r) `2 & (ff . r) `2 <= 1 ) by A116, SQUARE_1:112; :: thesis: verum
end;
case A118: ( 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 )
then A119: (Sq_Circ " ) . p1 = |[((p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| by Th38;
A120: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2 ) ) ) ) by A118, JGRAPH_2:23;
set pz = ff . r;
A121: ( (ff . r) `2 = (p1 `2 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) & (ff . r) `1 = (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) by A95, A96, A119, EUCLID:56;
A122: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A123: now
assume ( (ff . r) `2 = 0 & (ff . r) `1 = 0 ) ; :: thesis: contradiction
then p1 `2 = 0 by A121, A122, XCMPLX_1:6;
hence contradiction by A118; :: thesis: verum
end;
A125: now
( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) <= (- (p1 `2 )) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) ) by A120, A122, XREAL_1:66;
then ( ( p1 `1 <= p1 `2 & (- (p1 `2 )) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) <= (p1 `1 ) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) or ( (ff . r) `1 >= (ff . r) `2 & (ff . r) `1 <= - ((ff . r) `2 ) ) ) by A121, A122, XREAL_1:66;
hence ( ( (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 A121, A122, XREAL_1:66; :: thesis: verum
end;
A126: p1 = Sq_Circ . (ff . r) by A95, A96, Th54, FUNCT_1:54;
A127: 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 A121, A123, A125, Th14, JGRAPH_2:11;
A128: ( |[(((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 ))) & |[(((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;
A129: ((ff . r) `2 ) ^2 >= 0 by XREAL_1:65;
A130: 1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ) > 0 by Lm1;
|.p1.| ^2 <= |.p1.| by A96, SQUARE_1:111;
then A131: |.p1.| ^2 <= 1 by A96, XXREAL_0:2;
A132: (ff . r) `2 <> 0 by A121, A123, A125;
|.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 A126, A127, A128, 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 A130, 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 A130, 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 A130, A131, XREAL_1:66;
then (((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 ) <= 1 + ((((ff . r) `1 ) / ((ff . r) `2 )) ^2 ) by A130, 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 A129, XREAL_1:66;
then (((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) - 1) * (((ff . r) `2 ) ^2 ) <= ((ff . r) `1 ) ^2 by A132, XCMPLX_1:6, XCMPLX_1:88;
then A133: ((((ff . r) `2 ) ^2 ) - 1) * ((((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 )) <= 0 by Lm14;
A134: (((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 ) <> 0 by A123, COMPLEX1:2;
((ff . r) `1 ) ^2 >= 0 by XREAL_1:65;
then (((ff . r) `2 ) ^2 ) + (((ff . r) `1 ) ^2 ) >= 0 + 0 by A129;
then A135: (((ff . r) `2 ) ^2 ) - 1 <= 0 by A133, A134, XREAL_1:131;
then A136: ( (ff . r) `2 <= 1 & (ff . r) `2 >= - 1 ) by 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 A121, A125, 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 A136, 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 A136, 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 A135, SQUARE_1:112; :: thesis: verum
end;
end;
end;
A137: gg . r = (Sq_Circ " ) . (g . r) by A4, FUNCT_1:22;
g . r in rng g by A6, FUNCT_1:12;
then g . r in C0 by A1;
then consider p2 being Point of (TOP-REAL 2) such that
A138: ( g . r = p2 & |.p2.| <= 1 ) by A1;
now
per cases ( p2 = 0. (TOP-REAL 2) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ;
case p2 = 0. (TOP-REAL 2) ; :: thesis: ( - 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 A137, A138, Th38, JGRAPH_2:11; :: thesis: verum
end;
case A139: ( 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 )
then A140: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by Th38;
set px = gg . r;
set q = gg . r;
A141: ( (gg . r) `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & (gg . r) `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) by A137, A138, A140, EUCLID:56;
A142: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A146: now
( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) ) by A139, A142, XREAL_1:66;
then ( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( (gg . r) `2 >= (gg . r) `1 & (gg . r) `2 <= - ((gg . r) `1 ) ) ) by A141, A142, XREAL_1:66;
hence ( ( (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 A141, A142, XREAL_1:66; :: thesis: verum
end;
A147: p2 = Sq_Circ . (gg . r) by A137, A138, Th54, FUNCT_1:54;
A148: 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 A141, A143, A146, Def1, JGRAPH_2:11;
A149: ( |[(((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 ))) & |[(((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;
A150: ((gg . r) `1 ) ^2 >= 0 by XREAL_1:65;
A151: 1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ) > 0 by Lm1;
|.p2.| ^2 <= |.p2.| by A138, SQUARE_1:111;
then A152: |.p2.| ^2 <= 1 by A138, XXREAL_0:2;
A153: (gg . r) `1 <> 0 by A141, A143, A146;
|.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 A147, A148, A149, 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 A151, 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 A151, 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 A151, A152, XREAL_1:66;
then (((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 ) <= 1 + ((((gg . r) `2 ) / ((gg . r) `1 )) ^2 ) by A151, 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 A150, XREAL_1:66;
then (((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) - 1) * (((gg . r) `1 ) ^2 ) <= ((gg . r) `2 ) ^2 by A153, XCMPLX_1:6, XCMPLX_1:88;
then A154: ((((gg . r) `1 ) ^2 ) - 1) * ((((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 )) <= 0 by Lm14;
A155: (((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 ) <> 0 by A143, COMPLEX1:2;
((gg . r) `2 ) ^2 >= 0 by XREAL_1:65;
then (((gg . r) `1 ) ^2 ) + (((gg . r) `2 ) ^2 ) >= 0 + 0 by A150;
then A156: (((gg . r) `1 ) ^2 ) - 1 <= 0 by A154, A155, XREAL_1:131;
then A157: ( (gg . r) `1 <= 1 & (gg . r) `1 >= - 1 ) by SQUARE_1:112;
now
( ( (gg . r) `2 <= 1 & - (- ((gg . r) `1 )) >= - ((gg . r) `2 ) ) or ( (gg . r) `2 >= - 1 & (gg . r) `2 <= - ((gg . r) `1 ) ) ) by A141, A146, A157, 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 A157, XXREAL_0:2;
then ( ( (gg . r) `2 <= 1 & - 1 <= - (- ((gg . r) `2 )) ) or ( (gg . r) `2 >= - 1 & - ((gg . r) `2 ) >= - 1 ) ) by A157, XREAL_1:26, XXREAL_0:2;
hence ( ( (gg . r) `2 <= 1 & - 1 <= (gg . r) `2 ) or ( (gg . r) `2 >= - 1 & (gg . r) `2 <= 1 ) ) by XREAL_1:26; :: thesis: verum
end;
hence ( - 1 <= (gg . r) `1 & (gg . r) `1 <= 1 & - 1 <= (gg . r) `2 & (gg . r) `2 <= 1 ) by A156, SQUARE_1:112; :: thesis: verum
end;
case A158: ( 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 )
then A159: (Sq_Circ " ) . p2 = |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by Th38;
A160: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) ) by A158, JGRAPH_2:23;
set pz = gg . r;
A161: ( (gg . r) `2 = (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) & (gg . r) `1 = (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) by A137, A138, A159, EUCLID:56;
A162: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A163: now
assume ( (gg . r) `2 = 0 & (gg . r) `1 = 0 ) ; :: thesis: contradiction
then p2 `2 = 0 by A161, A162, XCMPLX_1:6;
hence contradiction by A158; :: thesis: verum
end;
A165: now
( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (- (p2 `2 )) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) ) by A160, A162, XREAL_1:66;
then ( ( p2 `1 <= p2 `2 & (- (p2 `2 )) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) or ( (gg . r) `1 >= (gg . r) `2 & (gg . r) `1 <= - ((gg . r) `2 ) ) ) by A161, A162, XREAL_1:66;
hence ( ( (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 A161, A162, XREAL_1:66; :: thesis: verum
end;
A166: p2 = Sq_Circ . (gg . r) by A137, A138, Th54, FUNCT_1:54;
A167: 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 A161, A163, A165, Th14, JGRAPH_2:11;
A168: ( |[(((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 ))) & |[(((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;
A169: ((gg . r) `2 ) ^2 >= 0 by XREAL_1:65;
A170: 1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ) > 0 by Lm1;
|.p2.| ^2 <= |.p2.| by A138, SQUARE_1:111;
then A171: |.p2.| ^2 <= 1 by A138, XXREAL_0:2;
A172: (gg . r) `2 <> 0 by A161, A163, A165;
|.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 A166, A167, A168, 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 A170, 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 A170, 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 A170, A171, XREAL_1:66;
then (((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 ) <= 1 + ((((gg . r) `1 ) / ((gg . r) `2 )) ^2 ) by A170, 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 A169, XREAL_1:66;
then (((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) - 1) * (((gg . r) `2 ) ^2 ) <= ((gg . r) `1 ) ^2 by A172, XCMPLX_1:6, XCMPLX_1:88;
then A173: ((((gg . r) `2 ) ^2 ) - 1) * ((((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 )) <= 0 by Lm14;
A174: (((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 ) <> 0 by A163, COMPLEX1:2;
((gg . r) `1 ) ^2 >= 0 by XREAL_1:65;
then (((gg . r) `2 ) ^2 ) + (((gg . r) `1 ) ^2 ) >= 0 + 0 by A169;
then A175: (((gg . r) `2 ) ^2 ) - 1 <= 0 by A173, A174, XREAL_1:131;
then A176: ( (gg . r) `2 <= 1 & (gg . r) `2 >= - 1 ) by 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 A161, A165, 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 A176, 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 A176, 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 A175, 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 A97; :: thesis: verum
end;
then rng ff meets rng gg by A1, A7, A9, A15, JGRAPH_1:65;
then A177: (rng ff) /\ (rng gg) <> {} by XBOOLE_0:def 7;
consider y being Element of (rng ff) /\ (rng gg);
A178: ( y in rng ff & y in rng gg ) by A177, XBOOLE_0:def 4;
then consider x1 being set such that
A179: ( x1 in dom ff & y = ff . x1 ) by FUNCT_1:def 5;
consider x2 being set such that
A180: ( x2 in dom gg & y = gg . x2 ) by A178, FUNCT_1:def 5;
A181: ff . x1 = (Sq_Circ " ) . (f . x1) by A179, FUNCT_1:22;
A182: dom (Sq_Circ " ) = the carrier of (TOP-REAL 2) by Th39, FUNCT_2:def 1;
x1 in dom f by A179, FUNCT_1:21;
then A183: f . x1 in rng f by FUNCT_1:def 5;
x2 in dom g by A180, FUNCT_1:21;
then A184: g . x2 in rng g by FUNCT_1:def 5;
gg . x2 = (Sq_Circ " ) . (g . x2) by A180, FUNCT_1:22;
then f . x1 = g . x2 by A179, A180, A181, A182, A183, A184, FUNCT_1:def 8;
then (rng f) /\ (rng g) <> {} by A183, A184, XBOOLE_0:def 4;
hence rng f meets rng g by XBOOLE_0:def 7; :: thesis: verum