let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom Sq_Circ or not x2 in dom 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 :: thesis: ( ( p2 = 0. (TOP-REAL 2) & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) & contradiction ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) & contradiction ) )

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:63;
then 1 + (((p2 `2) / (p2 `1)) ^2) >= 1 + 0 by XREAL_1:7;
then A7: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) >= 1 by SQUARE_1:18, SQUARE_1:26;
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:52, JGRAPH_2:3;
then A9: p2 `2 = 0 * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A7, XCMPLX_1:87
.= 0 ;
(p2 `1) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) = 0 by A3, A5, A8, EUCLID:52, JGRAPH_2:3;
then p2 `1 = 0 * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A7, XCMPLX_1:87
.= 0 ;
hence contradiction by A6, A9, EUCLID:53, EUCLID:54; :: 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:63;
then 1 + (((p2 `1) / (p2 `2)) ^2) >= 1 + 0 by XREAL_1:7;
then A11: sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) >= 1 by SQUARE_1:18, SQUARE_1:26;
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:52, JGRAPH_2:3;
then p2 `2 = 0 * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by A11, XCMPLX_1:87
.= 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:25;
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:52;
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:52;

now :: thesis: ( ( p2 = 0. (TOP-REAL 2) & contradiction ) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) & x1 = x2 ) )

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:63;
then 1 + (((p1 `2) / (p1 `1)) ^2) >= 1 + 0 by XREAL_1:7;
then A19: sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) >= 1 by SQUARE_1:18, SQUARE_1:26;
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:52, JGRAPH_2:3;
then A21: p1 `2 = 0 * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) by A19, XCMPLX_1:87
.= 0 ;
(p1 `1) / (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) = 0 by A3, A14, A20, EUCLID:52, JGRAPH_2:3;
then p1 `1 = 0 * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) by A19, XCMPLX_1:87
.= 0 ;
hence contradiction by A12, A21, EUCLID:53, EUCLID:54; :: 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 :: thesis: not p2 `1 = 0

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

end;

then A24: (p2 `1) ^2 > 0 by SQUARE_1:12;
A25: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by Lm1, SQUARE_1:25;
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:52;
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:76;
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:76;
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 2;
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 2;
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:52;
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:76;
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:76;
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 2;
then ((p2 `1) ^2) / (1 + (((p2 `2) / (p2 `1)) ^2)) = ((p1 `1) ^2) / (1 + (((p1 `2) / (p1 `1)) ^2)) by A16, SQUARE_1:def 2;
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:87;

now :: thesis: not p1 `1 = 0

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

end;

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

now :: thesis: ( ( p2 `2 = 0 & x1 = x2 ) or ( p2 `2 <> 0 & x1 = x2 ) )

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:53;
hence x1 = x2 by A35, EUCLID:53; :: thesis: verum

end;

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

then A36: (p2 `2) ^2 > 0 by SQUARE_1:12;
(((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:87;
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:74;
then (1 / ((p2 `1) ^2)) * ((p2 `2) ^2) = ((p1 `2) ^2) / ((p1 `1) ^2) by A36, XCMPLX_1:87;
then ((p2 `2) ^2) / ((p2 `1) ^2) = ((p1 `2) ^2) / ((p1 `1) ^2) by XCMPLX_1:99;
then ((p2 `2) / (p2 `1)) ^2 = ((p1 `2) ^2) / ((p1 `1) ^2) by XCMPLX_1:76;
then A37: 1 + (((p2 `2) / (p2 `1)) ^2) = 1 + (((p1 `2) / (p1 `1)) ^2) by XCMPLX_1:76;
then p2 `2 = ((p1 `2) / (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) by A28, A25, XCMPLX_1:87;
then A38: p2 `2 = p1 `2 by A13, XCMPLX_1:87;
p2 `1 = ((p1 `1) / (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) by A30, A25, A37, XCMPLX_1:87;
then p2 `1 = p1 `1 by A13, XCMPLX_1:87;
then p2 = |[(p1 `1),(p1 `2)]| by A38, EUCLID:53;
hence x1 = x2 by EUCLID:53; :: 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:13;
p2 `2 <> 0 by A39;
then A42: (p2 `2) ^2 > 0 by SQUARE_1:12;
|[((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:52;
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:76;
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:76;
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 2;
then ((p2 `2) ^2) / (1 + (((p2 `1) / (p2 `2)) ^2)) = ((p1 `2) ^2) / (1 + (((p1 `2) / (p1 `1)) ^2)) by A16, SQUARE_1:def 2;
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:87;
A45: sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
|[((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:52;
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:76;
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:76;
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 2;
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 2;

A48: now :: thesis: not p1 `1 = 0

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

end;

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

now :: thesis: ( ( p2 `1 = 0 & contradiction ) or ( p2 `1 <> 0 & x1 = x2 ) )

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

A55: now :: thesis: ( ( p1 `1 > 0 & ( ( (p1 `2) / (p1 `1) <= 1 & - 1 <= (p1 `2) / (p1 `1) ) or ( (p1 `2) / (p1 `1) >= 1 & (p1 `2) / (p1 `1) <= - 1 ) ) ) or ( p1 `1 < 0 & ( ( (p1 `2) / (p1 `1) <= 1 & - 1 <= (p1 `2) / (p1 `1) ) or ( (p1 `2) / (p1 `1) >= 1 & (p1 `2) / (p1 `1) <= - 1 ) ) ) )

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:72;
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:89;
(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:187; :: 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:197;
( ( (((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:73;
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:89; :: thesis: verum

end;

end;

end;

(p2 `1) ^2 > 0 by A52, SQUARE_1:12;
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:87;
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:74;
then (1 / ((p2 `1) ^2)) * ((p2 `2) ^2) = ((p1 `2) ^2) / ((p1 `1) ^2) by A42, XCMPLX_1:87;
then ((p2 `2) ^2) / ((p2 `1) ^2) = ((p1 `2) ^2) / ((p1 `1) ^2) by XCMPLX_1:99;
then ((p2 `2) / (p2 `1)) ^2 = ((p1 `2) ^2) / ((p1 `1) ^2) by XCMPLX_1:76;
then A60: ((p2 `2) / (p2 `1)) ^2 = ((p1 `2) / (p1 `1)) ^2 by XCMPLX_1:76;
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:40;

A62: now :: thesis: ( ( p2 `2 = ((p1 `2) / (p1 `1)) * (p2 `1) & ( 1 <= (p1 `2) / (p1 `1) or - 1 >= (p1 `2) / (p1 `1) ) ) or ( p2 `2 = (- ((p1 `2) / (p1 `1))) * (p2 `1) & ( 1 <= (p1 `2) / (p1 `1) or - 1 >= (p1 `2) / (p1 `1) ) ) )

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

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

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

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:72;
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:89;
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:187; :: 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:73;
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:89;
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:187; :: 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:24;
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 :: thesis: ( ( p2 `1 > 0 & ( ( 1 <= (p1 `2) / (p1 `1) & - ((p1 `2) / (p1 `1)) <= 1 ) or ( 1 >= (p1 `2) / (p1 `1) & 1 <= - ((p1 `2) / (p1 `1)) ) ) ) or ( p2 `1 < 0 & ( ( 1 <= (p1 `2) / (p1 `1) & - ((p1 `2) / (p1 `1)) <= 1 ) or ( 1 >= (p1 `2) / (p1 `1) & 1 <= - ((p1 `2) / (p1 `1)) ) ) ) )

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:72;
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:89, XCMPLX_1:187;
((- ((p1 `2) / (p1 `1))) * (p2 `1)) / (p2 `1) = - ((p1 `2) / (p1 `1)) by A52, XCMPLX_1:89;
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:73;
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:89, XCMPLX_1:187;
((- ((p1 `2) / (p1 `1))) * (p2 `1)) / (p2 `1) = - ((p1 `2) / (p1 `1)) by A52, XCMPLX_1:89;
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:24;
hence ( 1 <= (p1 `2) / (p1 `1) or - 1 >= (p1 `2) / (p1 `1) ) ; :: thesis: verum

end;

end;

end;

A69: now :: thesis: ( ( (p1 `2) / (p1 `1) = 1 & ((p2 `1) / (p2 `2)) ^2 = ((p1 `2) / (p1 `1)) ^2 ) or ( (p1 `2) / (p1 `1) = - 1 & ((p2 `1) / (p2 `2)) ^2 = ((p1 `2) / (p1 `1)) ^2 ) )

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:76;
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:76;
hence ((p2 `1) / (p2 `2)) ^2 = ((p1 `2) / (p1 `1)) ^2 by A60, A70, XCMPLX_1:76; :: 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:76;
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:76;
hence ((p2 `1) / (p2 `2)) ^2 = ((p1 `2) / (p1 `1)) ^2 by A60, A71, XCMPLX_1:76; :: 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:87;
then A72: p2 `2 = p1 `2 by A13, XCMPLX_1:87;
p2 `1 = ((p1 `1) / (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) by A46, A45, A69, XCMPLX_1:87;
then p2 `1 = p1 `1 by A13, XCMPLX_1:87;
then p2 = |[(p1 `1),(p1 `2)]| by A72, EUCLID:53;
hence x1 = x2 by EUCLID:53; :: 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:52;
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:52;
A76: 1 + (((p1 `1) / (p1 `2)) ^2) > 0 by Lm1;
A77: sqrt (1 + (((p1 `1) / (p1 `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
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:13;

now :: thesis: ( ( p2 = 0. (TOP-REAL 2) & contradiction ) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) & x1 = x2 ) )

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:63;
then 1 + (((p1 `1) / (p1 `2)) ^2) >= 1 + 0 by XREAL_1:7;
then A81: sqrt (1 + (((p1 `1) / (p1 `2)) ^2)) >= 1 by SQUARE_1:18, SQUARE_1:26;
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:52, JGRAPH_2:3;
then p1 `2 = 0 * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))) by A81, XCMPLX_1:87
.= 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 :: thesis: not p2 `1 = 0

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

end;

then A84: (p2 `1) ^2 > 0 by SQUARE_1:12;
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:52;
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:76;
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:76;
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 2;
then ((p2 `1) ^2) / (1 + (((p2 `2) / (p2 `1)) ^2)) = ((p1 `1) ^2) / (1 + (((p1 `1) / (p1 `2)) ^2)) by A76, SQUARE_1:def 2;
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:87;
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:52;
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:76;
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:76;
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 2;
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 2;
A91: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by Lm1, SQUARE_1:25;
A92: p1 `2 <> 0 by A73;
then A93: (p1 `2) ^2 > 0 by SQUARE_1:12;

now :: thesis: ( ( p2 `2 = 0 & contradiction ) or ( p2 `2 <> 0 & x1 = x2 ) )

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:87;

A97: now :: thesis: ( ( p1 `2 > 0 & ( ( (p1 `1) / (p1 `2) <= 1 & - 1 <= (p1 `1) / (p1 `2) ) or ( (p1 `1) / (p1 `2) >= 1 & (p1 `1) / (p1 `2) <= - 1 ) ) ) or ( p1 `2 < 0 & ( ( (p1 `1) / (p1 `2) <= 1 & - 1 <= (p1 `1) / (p1 `2) ) or ( (p1 `1) / (p1 `2) >= 1 & (p1 `1) / (p1 `2) <= - 1 ) ) ) )

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:197;
( ( (((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:72;
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:89; :: 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:73;
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:89;
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:197; :: thesis: verum

end;

end;

end;

(p2 `2) ^2 > 0 by A94, SQUARE_1:12;
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:87;
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:74;
then (1 / ((p2 `2) ^2)) * ((p2 `1) ^2) = ((p1 `1) ^2) / ((p1 `2) ^2) by A84, XCMPLX_1:87;
then ((p2 `1) ^2) / ((p2 `2) ^2) = ((p1 `1) ^2) / ((p1 `2) ^2) by XCMPLX_1:99;
then ((p2 `1) / (p2 `2)) ^2 = ((p1 `1) ^2) / ((p1 `2) ^2) by XCMPLX_1:76;
then A101: ((p2 `1) / (p2 `2)) ^2 = ((p1 `1) / (p1 `2)) ^2 by XCMPLX_1:76;
then A102: ( (p2 `1) / (p2 `2) = (p1 `1) / (p1 `2) or (p2 `1) / (p2 `2) = - ((p1 `1) / (p1 `2)) ) by SQUARE_1:40;

A103: now :: thesis: ( ( p2 `1 = ((p1 `1) / (p1 `2)) * (p2 `2) & ( 1 <= (p1 `1) / (p1 `2) or - 1 >= (p1 `1) / (p1 `2) ) ) or ( p2 `1 = (- ((p1 `1) / (p1 `2))) * (p2 `2) & ( 1 <= (p1 `1) / (p1 `2) or - 1 >= (p1 `1) / (p1 `2) ) ) )

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

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

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

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:72;
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:89;
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:187; :: 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:73;
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:89;
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:187; :: 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:24;
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 :: thesis: ( ( p2 `2 > 0 & ( ( 1 <= (p1 `1) / (p1 `2) & - ((p1 `1) / (p1 `2)) <= 1 ) or ( 1 >= (p1 `1) / (p1 `2) & 1 <= - ((p1 `1) / (p1 `2)) ) ) ) or ( p2 `2 < 0 & ( ( 1 <= (p1 `1) / (p1 `2) & - ((p1 `1) / (p1 `2)) <= 1 ) or ( 1 >= (p1 `1) / (p1 `2) & 1 <= - ((p1 `1) / (p1 `2)) ) ) ) )

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:72;
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:89, XCMPLX_1:187;
((- ((p1 `1) / (p1 `2))) * (p2 `2)) / (p2 `2) = - ((p1 `1) / (p1 `2)) by A94, XCMPLX_1:89;
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:73;
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:89, XCMPLX_1:187;
((- ((p1 `1) / (p1 `2))) * (p2 `2)) / (p2 `2) = - ((p1 `1) / (p1 `2)) by A94, XCMPLX_1:89;
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:24;
hence ( 1 <= (p1 `1) / (p1 `2) or - 1 >= (p1 `1) / (p1 `2) ) ; :: thesis: verum

end;

end;

end;

A110: now :: thesis: ( ( (p1 `1) / (p1 `2) = 1 & ((p2 `2) / (p2 `1)) ^2 = ((p1 `1) / (p1 `2)) ^2 ) or ( (p1 `1) / (p1 `2) = - 1 & ((p2 `2) / (p2 `1)) ^2 = ((p1 `1) / (p1 `2)) ^2 ) )

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:76;
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:76;
hence ((p2 `2) / (p2 `1)) ^2 = ((p1 `1) / (p1 `2)) ^2 by A101, A111, XCMPLX_1:76; :: 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:76;
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:76;
hence ((p2 `2) / (p2 `1)) ^2 = ((p1 `1) / (p1 `2)) ^2 by A101, A112, XCMPLX_1:76; :: 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:87;
then A113: p2 `1 = p1 `1 by A77, XCMPLX_1:87;
p2 `2 = ((p1 `2) / (sqrt (1 + (((p1 `1) / (p1 `2)) ^2)))) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))) by A89, A91, A110, XCMPLX_1:87;
then p2 `2 = p1 `2 by A77, XCMPLX_1:87;
then p2 = |[(p1 `1),(p1 `2)]| by A113, EUCLID:53;
hence x1 = x2 by EUCLID:53; :: 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:12;
A116: sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
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:52;
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:76;
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:76;
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 2;
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 2;
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:52;
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:76;
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:76;
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 2;
then ((p2 `2) ^2) / (1 + (((p2 `1) / (p2 `2)) ^2)) = ((p1 `2) ^2) / (1 + (((p1 `1) / (p1 `2)) ^2)) by A76, SQUARE_1:def 2;
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:87;
p1 `2 <> 0 by A73;
then A123: (p1 `2) ^2 > 0 by SQUARE_1:12;

now :: thesis: ( ( p2 `1 = 0 & x1 = x2 ) or ( p2 `1 <> 0 & x1 = x2 ) )

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:53;
hence x1 = x2 by A125, EUCLID:53; :: thesis: verum

end;

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

then A126: (p2 `1) ^2 > 0 by SQUARE_1:12;
(((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:87;
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:74;
then (1 / ((p2 `2) ^2)) * ((p2 `1) ^2) = ((p1 `1) ^2) / ((p1 `2) ^2) by A126, XCMPLX_1:87;
then ((p2 `1) ^2) / ((p2 `2) ^2) = ((p1 `1) ^2) / ((p1 `2) ^2) by XCMPLX_1:99;
then ((p2 `1) / (p2 `2)) ^2 = ((p1 `1) ^2) / ((p1 `2) ^2) by XCMPLX_1:76;
then A127: 1 + (((p2 `1) / (p2 `2)) ^2) = 1 + (((p1 `1) / (p1 `2)) ^2) by XCMPLX_1:76;
then p2 `1 = ((p1 `1) / (sqrt (1 + (((p1 `1) / (p1 `2)) ^2)))) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))) by A119, A116, XCMPLX_1:87;
then A128: p2 `1 = p1 `1 by A77, XCMPLX_1:87;
p2 `2 = ((p1 `2) / (sqrt (1 + (((p1 `1) / (p1 `2)) ^2)))) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))) by A121, A116, A127, XCMPLX_1:87;
then p2 `2 = p1 `2 by A77, XCMPLX_1:87;
then p2 = |[(p1 `1),(p1 `2)]| by A128, EUCLID:53;
hence x1 = x2 by EUCLID:53; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;