let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 Sq_Circ or not x2 in proj1 Sq_Circ or not Sq_Circ . x1 = Sq_Circ . x2 or x1 = x2 )
assume that
A1: x1 in dom Sq_Circ and
A2: x2 in dom Sq_Circ and
A3: Sq_Circ . x1 = Sq_Circ . x2 ; :: thesis: x1 = x2
reconsider p2 = x2 as Point of (TOP-REAL 2) by A2;
reconsider p1 = x1 as Point of (TOP-REAL 2) by A1;
set q = p1;
set p = p2;

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 ) ) ) ) ;

suppose A4: p1 = 0. (TOP-REAL 2) ; :: thesis: x1 = x2

then A5: Sq_Circ . p1 = 0. (TOP-REAL 2) by Def1;

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: x1 = x2

hence x1 = x2 by A4; :: thesis: verum

end;

case A6: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: contradiction

((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A7: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
A8: Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A6, Def1;
then (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 by A3, A5, EUCLID:56, JGRAPH_2:11;
then A9: p2 `2 = 0 * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A7, XCMPLX_1:88
.= 0 ;
(p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 by A3, A5, A8, EUCLID:56, JGRAPH_2:11;
then p2 `1 = 0 * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A7, XCMPLX_1:88
.= 0 ;
hence contradiction by A6, A9, EUCLID:57, EUCLID:58; :: thesis: verum

end;

case A10: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: contradiction

((p2 `1 ) / (p2 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A11: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A10, Def1;
then (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 by A3, A5, EUCLID:56, JGRAPH_2:11;
then p2 `2 = 0 * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A11, XCMPLX_1:88
.= 0 ;
hence contradiction by A10; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

suppose A12: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) ; :: thesis: x1 = x2

A13: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A14: Sq_Circ . p1 = |[((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by A12, Def1;
A15: |[((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| `2 = (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by EUCLID:56;
A16: 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) > 0 by Lm1;
A17: |[((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| `1 = (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by EUCLID:56;

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 A18: p2 = 0. (TOP-REAL 2) ; :: thesis: contradiction

((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A19: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
A20: Sq_Circ . p2 = 0. (TOP-REAL 2) by A18, Def1;
then (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) = 0 by A3, A14, EUCLID:56, JGRAPH_2:11;
then A21: p1 `2 = 0 * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A19, XCMPLX_1:88
.= 0 ;
(p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) = 0 by A3, A14, A20, EUCLID:56, JGRAPH_2:11;
then p1 `1 = 0 * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A19, XCMPLX_1:88
.= 0 ;
hence contradiction by A12, A21, EUCLID:57, EUCLID:58; :: thesis: verum

end;

case A22: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: x1 = x2

now

assume A23: p2 `1 = 0 ; :: thesis: contradiction
then p2 `2 = 0 by A22;
hence contradiction by A22, A23, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A24: (p2 `1 ) ^2 > 0 by SQUARE_1:74;
A25: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A26: 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) > 0 by Lm1;
A27: Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A22, Def1;
then A28: (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A3, A14, A15, EUCLID:56;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A26, SQUARE_1:def 4;
then A29: ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A16, SQUARE_1:def 4;
A30: (p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A3, A14, A17, A27, EUCLID:56;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A26, SQUARE_1:def 4;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A16, SQUARE_1:def 4;
then (((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A24, XCMPLX_1:60;
then A31: (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A16, XCMPLX_1:88;

now

assume A32: p1 `1 = 0 ; :: thesis: contradiction
then p1 `2 = 0 by A12;
hence contradiction by A12, A32, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A33: (p1 `1 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `2 = 0 or p2 `2 <> 0 ) ;

case A34: p2 `2 = 0 ; :: thesis: x1 = x2

then (p1 `2 ) ^2 = 0 by A16, A29, XCMPLX_1:50;
then A35: p1 `2 = 0 by XCMPLX_1:6;
then p2 = |[(p1 `1 ),0 ]| by A3, A14, A27, A34, EUCLID:57, SQUARE_1:83;
hence x1 = x2 by A35, EUCLID:57; :: thesis: verum

end;

case p2 `2 <> 0 ; :: thesis: x1 = x2

then A36: (p2 `2 ) ^2 > 0 by SQUARE_1:74;
(((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A29, XCMPLX_1:48;
then (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A36, XCMPLX_1:60;
then (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A16, XCMPLX_1:88;
then (((p1 `1 ) ^2 ) / ((p1 `1 ) ^2 )) / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A31, XCMPLX_1:48;
then 1 / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A33, XCMPLX_1:60;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = (((p2 `2 ) ^2 ) * (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ))) / ((p1 `1 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by A36, XCMPLX_1:88;
then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:100;
then ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:77;
then A37: 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) = 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) by XCMPLX_1:77;
then p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A28, A25, XCMPLX_1:88;
then A38: p2 `2 = p1 `2 by A13, XCMPLX_1:88;
p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A30, A25, A37, XCMPLX_1:88;
then p2 `1 = p1 `1 by A13, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A38, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case A39: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: x1 = x2

A40: 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) > 0 by Lm1;
A41: ( ( p2 <> 0. (TOP-REAL 2) & p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) by A39, JGRAPH_2:23;
p2 `2 <> 0 by A39;
then A42: (p2 `2 ) ^2 > 0 by SQUARE_1:74;
|[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 = (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by EUCLID:56;
then A43: (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A3, A14, A15, A39, Def1;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A40, SQUARE_1:def 4;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A16, SQUARE_1:def 4;
then (((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A42, XCMPLX_1:60;
then A44: (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A16, XCMPLX_1:88;
A45: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
|[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 = (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by EUCLID:56;
then A46: (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A3, A14, A17, A39, Def1;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A40, SQUARE_1:def 4;
then A47: ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A16, SQUARE_1:def 4;

A48: now

assume A49: p1 `1 = 0 ; :: thesis: contradiction
then p1 `2 = 0 by A12;
hence contradiction by A12, A49, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A50: (p1 `1 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `1 = 0 or p2 `1 <> 0 ) ;

case p2 `1 = 0 ; :: thesis: contradiction

then (p1 `1 ) ^2 = 0 by A16, A47, XCMPLX_1:50;
then A51: p1 `1 = 0 by XCMPLX_1:6;
then p1 `2 = 0 by A12;
hence contradiction by A12, A51, EUCLID:57, EUCLID:58; :: thesis: verum

end;

case A52: p2 `1 <> 0 ; :: thesis: x1 = x2

set a = (p1 `2 ) / (p1 `1 );
(((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A47, XCMPLX_1:48;
then A53: (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
A54: ( ( (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) <= p1 `1 & - (p1 `1 ) <= (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) ) or ( (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) >= p1 `1 & (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) <= - (p1 `1 ) ) ) by A12, A48, XCMPLX_1:88;

A55: now

per cases ( p1 `1 > 0 or p1 `1 < 0 ) by A48;

case A56: p1 `1 > 0 ; :: thesis: ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) )

then ( ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) <= (p1 `1 ) / (p1 `1 ) & (- (p1 `1 )) / (p1 `1 ) <= (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) ) or ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) >= (p1 `1 ) / (p1 `1 ) & (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) <= (- (p1 `1 )) / (p1 `1 ) ) ) by A54, XREAL_1:74;
then A57: ( ( (p1 `2 ) / (p1 `1 ) <= (p1 `1 ) / (p1 `1 ) & (- (p1 `1 )) / (p1 `1 ) <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= (p1 `1 ) / (p1 `1 ) & (p1 `2 ) / (p1 `1 ) <= (- (p1 `1 )) / (p1 `1 ) ) ) by A56, XCMPLX_1:90;
(p1 `1 ) / (p1 `1 ) = 1 by A56, XCMPLX_1:60;
hence ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) ) by A57, XCMPLX_1:188; :: thesis: verum

end;

case A58: p1 `1 < 0 ; :: thesis: ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) )

then A59: ( (p1 `1 ) / (p1 `1 ) = 1 & (- (p1 `1 )) / (p1 `1 ) = - 1 ) by XCMPLX_1:60, XCMPLX_1:198;
( ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) >= (p1 `1 ) / (p1 `1 ) & (- (p1 `1 )) / (p1 `1 ) >= (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) ) or ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) <= (p1 `1 ) / (p1 `1 ) & (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) >= (- (p1 `1 )) / (p1 `1 ) ) ) by A54, A58, XREAL_1:75;
hence ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) ) by A58, A59, XCMPLX_1:90; :: thesis: verum

end;

end;

end;

(p2 `1 ) ^2 > 0 by A52, SQUARE_1:74;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A53, XCMPLX_1:60;
then (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A16, XCMPLX_1:88;
then (((p1 `1 ) ^2 ) / ((p1 `1 ) ^2 )) / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A44, XCMPLX_1:48;
then 1 / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A50, XCMPLX_1:60;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = (((p2 `2 ) ^2 ) * (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ))) / ((p1 `1 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by A42, XCMPLX_1:88;
then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:100;
then ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:77;
then A60: ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2 by XCMPLX_1:77;
then A61: ( ((p2 `2 ) / (p2 `1 )) * (p2 `1 ) = ((p1 `2 ) / (p1 `1 )) * (p2 `1 ) or ((p2 `2 ) / (p2 `1 )) * (p2 `1 ) = (- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ) ) by SQUARE_1:109;

A62: now

per cases ( p2 `2 = ((p1 `2 ) / (p1 `1 )) * (p2 `1 ) or p2 `2 = (- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ) ) by A52, A61, XCMPLX_1:88;

case A63: p2 `2 = ((p1 `2 ) / (p1 `1 )) * (p2 `1 ) ; :: thesis: ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) )

now

per cases ( p2 `1 > 0 or p2 `1 < 0 ) by A52;

case p2 `1 > 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) <= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) <= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A41, A63, XREAL_1:74;
then A64: ( ( 1 <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) <= 1 ) or ( 1 >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & 1 <= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A52, XCMPLX_1:60;
(((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) = (p1 `2 ) / (p1 `1 ) by A52, XCMPLX_1:90;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A64, XCMPLX_1:188; :: thesis: verum

end;

case p2 `1 < 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) >= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) >= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A41, A63, XREAL_1:75;
then A65: ( ( 1 >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) >= 1 ) or ( 1 <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & 1 >= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A52, XCMPLX_1:60;
(((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) = (p1 `2 ) / (p1 `1 ) by A52, XCMPLX_1:90;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A65, XCMPLX_1:188; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & - 1 >= - (- ((p1 `2 ) / (p1 `1 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) ) ; :: thesis: verum

end;

case A66: p2 `2 = (- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ) ; :: thesis: ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) )

now

per cases ( p2 `1 > 0 or p2 `1 < 0 ) by A52;

case p2 `1 > 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) <= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) <= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A41, A66, XREAL_1:74;
then ( ( 1 <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) <= 1 ) or ( 1 >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & 1 <= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A52, XCMPLX_1:60;
then A67: ( ( 1 <= - ((p1 `2 ) / (p1 `1 )) & - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) <= 1 ) or ( 1 >= - ((p1 `2 ) / (p1 `1 )) & 1 <= - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) ) ) by A52, XCMPLX_1:90, XCMPLX_1:188;
((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) = - ((p1 `2 ) / (p1 `1 )) by A52, XCMPLX_1:90;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A67; :: thesis: verum

end;

case p2 `1 < 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) >= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) >= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A41, A66, XREAL_1:75;
then ( ( 1 >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) >= 1 ) or ( 1 <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & 1 >= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A52, XCMPLX_1:60;
then A68: ( ( 1 >= - ((p1 `2 ) / (p1 `1 )) & - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) >= 1 ) or ( 1 <= - ((p1 `2 ) / (p1 `1 )) & 1 >= - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) ) ) by A52, XCMPLX_1:90, XCMPLX_1:188;
((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) = - ((p1 `2 ) / (p1 `1 )) by A52, XCMPLX_1:90;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A68; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & - 1 >= - (- ((p1 `2 ) / (p1 `1 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) ) ; :: thesis: verum

end;

end;

end;

A69: now

per cases ( (p1 `2 ) / (p1 `1 ) = 1 or (p1 `2 ) / (p1 `1 ) = - 1 ) by A62, A55, XXREAL_0:1;

case (p1 `2 ) / (p1 `1 ) = 1 ; :: thesis: ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2

then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = 1 by A60, XCMPLX_1:77;
then A70: (p2 `2 ) ^2 = (p2 `1 ) ^2 by XCMPLX_1:58;
((p2 `1 ) / (p2 `2 )) ^2 = ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2 by A60, A70, XCMPLX_1:77; :: thesis: verum

end;

case (p1 `2 ) / (p1 `1 ) = - 1 ; :: thesis: ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2

then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = 1 by A60, XCMPLX_1:77;
then A71: (p2 `2 ) ^2 = (p2 `1 ) ^2 by XCMPLX_1:58;
((p2 `1 ) / (p2 `2 )) ^2 = ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2 by A60, A71, XCMPLX_1:77; :: thesis: verum

end;

end;

end;

then p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A43, A45, XCMPLX_1:88;
then A72: p2 `2 = p1 `2 by A13, XCMPLX_1:88;
p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A46, A45, A69, XCMPLX_1:88;
then p2 `1 = p1 `1 by A13, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A72, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

suppose A73: ( p1 <> 0. (TOP-REAL 2) & not ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) & not ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ; :: thesis: x1 = x2

A74: |[((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| `2 = (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by EUCLID:56;
A75: |[((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| `1 = (p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by EUCLID:56;
A76: 1 + (((p1 `1 ) / (p1 `2 )) ^2 ) > 0 by Lm1;
A77: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A78: Sq_Circ . p1 = |[((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| by A73, Def1;
A79: ( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2 ) ) ) by A73, JGRAPH_2:23;

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 A80: p2 = 0. (TOP-REAL 2) ; :: thesis: contradiction

((p1 `1 ) / (p1 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `1 ) / (p1 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A81: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
Sq_Circ . p2 = 0. (TOP-REAL 2) by A80, Def1;
then (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) = 0 by A3, A78, EUCLID:56, JGRAPH_2:11;
then p1 `2 = 0 * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A81, XCMPLX_1:88
.= 0 ;
hence contradiction by A73; :: thesis: verum

end;

case A82: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: x1 = x2

now

assume A83: p2 `1 = 0 ; :: thesis: contradiction
then p2 `2 = 0 by A82;
hence contradiction by A82, A83, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A84: (p2 `1 ) ^2 > 0 by SQUARE_1:74;
A85: 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) > 0 by Lm1;
A86: Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A82, Def1;
then A87: (p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A3, A78, A75, EUCLID:56;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A85, SQUARE_1:def 4;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A76, SQUARE_1:def 4;
then (((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A84, XCMPLX_1:60;
then A88: (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A76, XCMPLX_1:88;
A89: (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A3, A78, A74, A86, EUCLID:56;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A85, SQUARE_1:def 4;
then A90: ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A76, SQUARE_1:def 4;
A91: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A92: p1 `2 <> 0 by A73;
then A93: (p1 `2 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `2 = 0 or p2 `2 <> 0 ) ;

case p2 `2 = 0 ; :: thesis: contradiction

then (p1 `2 ) ^2 = 0 by A76, A90, XCMPLX_1:50;
then p1 `2 = 0 by XCMPLX_1:6;
hence contradiction by A73; :: thesis: verum

end;

case A94: p2 `2 <> 0 ; :: thesis: x1 = x2

set a = (p1 `1 ) / (p1 `2 );
(((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A90, XCMPLX_1:48;
then A95: (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
A96: ( ( (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) <= p1 `2 & - (p1 `2 ) <= (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) ) or ( (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) >= p1 `2 & (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) <= - (p1 `2 ) ) ) by A79, A92, XCMPLX_1:88;

A97: now

per cases ( p1 `2 > 0 or p1 `2 < 0 ) by A73;

case A98: p1 `2 > 0 ; :: thesis: ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) )

then A99: ( (p1 `2 ) / (p1 `2 ) = 1 & (- (p1 `2 )) / (p1 `2 ) = - 1 ) by XCMPLX_1:60, XCMPLX_1:198;
( ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) <= (p1 `2 ) / (p1 `2 ) & (- (p1 `2 )) / (p1 `2 ) <= (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) ) or ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) >= (p1 `2 ) / (p1 `2 ) & (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) <= (- (p1 `2 )) / (p1 `2 ) ) ) by A96, A98, XREAL_1:74;
hence ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) ) by A98, A99, XCMPLX_1:90; :: thesis: verum

end;

case A100: p1 `2 < 0 ; :: thesis: ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) )

then ( ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) >= (p1 `2 ) / (p1 `2 ) & (- (p1 `2 )) / (p1 `2 ) >= (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) ) or ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) <= (p1 `2 ) / (p1 `2 ) & (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) >= (- (p1 `2 )) / (p1 `2 ) ) ) by A96, XREAL_1:75;
then ( ( (p1 `1 ) / (p1 `2 ) >= (p1 `2 ) / (p1 `2 ) & (- (p1 `2 )) / (p1 `2 ) >= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) <= (p1 `2 ) / (p1 `2 ) & (p1 `1 ) / (p1 `2 ) >= (- (p1 `2 )) / (p1 `2 ) ) ) by A100, XCMPLX_1:90;
hence ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) ) by A100, XCMPLX_1:60, XCMPLX_1:198; :: thesis: verum

end;

end;

end;

(p2 `2 ) ^2 > 0 by A94, SQUARE_1:74;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A95, XCMPLX_1:60;
then (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A76, XCMPLX_1:88;
then (((p1 `2 ) ^2 ) / ((p1 `2 ) ^2 )) / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A88, XCMPLX_1:48;
then 1 / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A93, XCMPLX_1:60;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = (((p2 `1 ) ^2 ) * (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ))) / ((p1 `2 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by A84, XCMPLX_1:88;
then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:100;
then ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:77;
then A101: ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2 by XCMPLX_1:77;
then A102: ( (p2 `1 ) / (p2 `2 ) = (p1 `1 ) / (p1 `2 ) or (p2 `1 ) / (p2 `2 ) = - ((p1 `1 ) / (p1 `2 )) ) by SQUARE_1:109;

A103: now

per cases ( p2 `1 = ((p1 `1 ) / (p1 `2 )) * (p2 `2 ) or p2 `1 = (- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ) ) by A94, A102, XCMPLX_1:88;

case A104: p2 `1 = ((p1 `1 ) / (p1 `2 )) * (p2 `2 ) ; :: thesis: ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) )

now

per cases ( p2 `2 > 0 or p2 `2 < 0 ) by A94;

case p2 `2 > 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) <= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) <= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A82, A104, XREAL_1:74;
then A105: ( ( 1 <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) <= 1 ) or ( 1 >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & 1 <= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
(((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) = (p1 `1 ) / (p1 `2 ) by A94, XCMPLX_1:90;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A105, XCMPLX_1:188; :: thesis: verum

end;

case p2 `2 < 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) >= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) >= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A82, A104, XREAL_1:75;
then A106: ( ( 1 >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) >= 1 ) or ( 1 <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & 1 >= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
(((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) = (p1 `1 ) / (p1 `2 ) by A94, XCMPLX_1:90;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A106, XCMPLX_1:188; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & - 1 >= - (- ((p1 `1 ) / (p1 `2 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) ) ; :: thesis: verum

end;

case A107: p2 `1 = (- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ) ; :: thesis: ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) )

now

per cases ( p2 `2 > 0 or p2 `2 < 0 ) by A94;

case p2 `2 > 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) <= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) <= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A82, A107, XREAL_1:74;
then ( ( 1 <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) <= 1 ) or ( 1 >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & 1 <= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
then A108: ( ( 1 <= - ((p1 `1 ) / (p1 `2 )) & - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) <= 1 ) or ( 1 >= - ((p1 `1 ) / (p1 `2 )) & 1 <= - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) ) ) by A94, XCMPLX_1:90, XCMPLX_1:188;
((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) = - ((p1 `1 ) / (p1 `2 )) by A94, XCMPLX_1:90;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A108; :: thesis: verum

end;

case p2 `2 < 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) >= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) >= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A82, A107, XREAL_1:75;
then ( ( 1 >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) >= 1 ) or ( 1 <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & 1 >= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
then A109: ( ( 1 >= - ((p1 `1 ) / (p1 `2 )) & - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) >= 1 ) or ( 1 <= - ((p1 `1 ) / (p1 `2 )) & 1 >= - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) ) ) by A94, XCMPLX_1:90, XCMPLX_1:188;
((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) = - ((p1 `1 ) / (p1 `2 )) by A94, XCMPLX_1:90;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A109; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & - 1 >= - (- ((p1 `1 ) / (p1 `2 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) ) ; :: thesis: verum

end;

end;

end;

A110: now

per cases ( (p1 `1 ) / (p1 `2 ) = 1 or (p1 `1 ) / (p1 `2 ) = - 1 ) by A103, A97, XXREAL_0:1;

case (p1 `1 ) / (p1 `2 ) = 1 ; :: thesis: ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2

then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = 1 by A101, XCMPLX_1:77;
then A111: (p2 `1 ) ^2 = (p2 `2 ) ^2 by XCMPLX_1:58;
((p2 `2 ) / (p2 `1 )) ^2 = ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2 by A101, A111, XCMPLX_1:77; :: thesis: verum

end;

case (p1 `1 ) / (p1 `2 ) = - 1 ; :: thesis: ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2

then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = 1 by A101, XCMPLX_1:77;
then A112: (p2 `1 ) ^2 = (p2 `2 ) ^2 by XCMPLX_1:58;
((p2 `2 ) / (p2 `1 )) ^2 = ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2 by A101, A112, XCMPLX_1:77; :: thesis: verum

end;

end;

end;

then p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A87, A91, XCMPLX_1:88;
then A113: p2 `1 = p1 `1 by A77, XCMPLX_1:88;
p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A89, A91, A110, XCMPLX_1:88;
then p2 `2 = p1 `2 by A77, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A113, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case A114: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: x1 = x2

then p2 `2 <> 0 ;
then A115: (p2 `2 ) ^2 > 0 by SQUARE_1:74;
A116: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A117: 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) > 0 by Lm1;
A118: Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A114, Def1;
then A119: (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A3, A78, A75, EUCLID:56;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A117, SQUARE_1:def 4;
then A120: ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A76, SQUARE_1:def 4;
A121: (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A3, A78, A74, A118, EUCLID:56;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A117, SQUARE_1:def 4;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A76, SQUARE_1:def 4;
then (((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A115, XCMPLX_1:60;
then A122: (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A76, XCMPLX_1:88;
p1 `2 <> 0 by A73;
then A123: (p1 `2 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `1 = 0 or p2 `1 <> 0 ) ;

case A124: p2 `1 = 0 ; :: thesis: x1 = x2

then (p1 `1 ) ^2 = 0 by A76, A120, XCMPLX_1:50;
then A125: p1 `1 = 0 by XCMPLX_1:6;
then p2 = |[0 ,(p1 `2 )]| by A3, A78, A118, A124, EUCLID:57, SQUARE_1:83;
hence x1 = x2 by A125, EUCLID:57; :: thesis: verum

end;

case p2 `1 <> 0 ; :: thesis: x1 = x2

then A126: (p2 `1 ) ^2 > 0 by SQUARE_1:74;
(((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A120, XCMPLX_1:48;
then (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A126, XCMPLX_1:60;
then (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A76, XCMPLX_1:88;
then (((p1 `2 ) ^2 ) / ((p1 `2 ) ^2 )) / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A122, XCMPLX_1:48;
then 1 / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A123, XCMPLX_1:60;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = (((p2 `1 ) ^2 ) * (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ))) / ((p1 `2 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by A126, XCMPLX_1:88;
then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:100;
then ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:77;
then A127: 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) = 1 + (((p1 `1 ) / (p1 `2 )) ^2 ) by XCMPLX_1:77;
then p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A119, A116, XCMPLX_1:88;
then A128: p2 `1 = p1 `1 by A77, XCMPLX_1:88;
p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A121, A116, A127, XCMPLX_1:88;
then p2 `2 = p1 `2 by A77, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A128, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;