let cn be Real; ( - 1 < cn & cn < 1 implies cn -FanMorphS is one-to-one )
assume that
A1:
- 1 < cn
and
A2:
cn < 1
; cn -FanMorphS is one-to-one
for x1, x2 being set st x1 in dom (cn -FanMorphS ) & x2 in dom (cn -FanMorphS ) & (cn -FanMorphS ) . x1 = (cn -FanMorphS ) . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
( x1 in dom (cn -FanMorphS ) & x2 in dom (cn -FanMorphS ) & (cn -FanMorphS ) . x1 = (cn -FanMorphS ) . x2 implies x1 = x2 )
assume that A3:
x1 in dom (cn -FanMorphS )
and A4:
x2 in dom (cn -FanMorphS )
and A5:
(cn -FanMorphS ) . x1 = (cn -FanMorphS ) . x2
;
x1 = x2
reconsider p2 =
x2 as
Point of
(TOP-REAL 2) by A4;
reconsider p1 =
x1 as
Point of
(TOP-REAL 2) by A3;
set q =
p1;
set p =
p2;
A6:
1
- cn > 0
by A2, XREAL_1:151;
per cases
( p1 `2 >= 0 or ( (p1 `1 ) / |.p1.| >= cn & p1 `2 <= 0 & p1 <> 0. (TOP-REAL 2) ) or ( (p1 `1 ) / |.p1.| < cn & p1 `2 <= 0 & p1 <> 0. (TOP-REAL 2) ) )
by JGRAPH_2:11;
suppose A7:
p1 `2 >= 0
;
x1 = x2then A8:
(cn -FanMorphS ) . p1 = p1
by Th120;
per cases
( p2 `2 >= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| >= cn & p2 `2 <= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| < cn & p2 `2 <= 0 ) )
by JGRAPH_2:11;
suppose A9:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| >= cn &
p2 `2 <= 0 )
;
x1 = x2then A10:
|.p2.| <> 0
by TOPRNS_1:25;
then A11:
|.p2.| ^2 > 0
by SQUARE_1:74;
A12:
((p2 `1 ) / |.p2.|) - cn >= 0
by A9, XREAL_1:50;
A13:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by XREAL_1:9;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by A13, XREAL_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A11, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p2 `1 ) / |.p2.|
by SQUARE_1:121;
then
1
- cn >= ((p2 `1 ) / |.p2.|) - cn
by XREAL_1:11;
then
- (1 - cn) <= - (((p2 `1 ) / |.p2.|) - cn)
by XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A6, XREAL_1:74;
then A14:
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A6, XCMPLX_1:198;
A15:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|
by A1, A2, A9, Th122;
then A16:
p1 `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))))
by A5, A8, EUCLID:56;
((p2 `1 ) / |.p2.|) - cn >= 0
by A9, XREAL_1:50;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A6, A14, SQUARE_1:119;
then A17:
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 )) >= 0
by SQUARE_1:def 4;
then
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) ^2 ) / ((1 - cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) ^2 ) / ((1 - cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
p1 `2 = 0
by A5, A7, A8, A15, EUCLID:56;
then A18:
- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))) = - 0
by A16, A10, XCMPLX_1:6;
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))) ^2 ) >= 0
by A17, XCMPLX_1:188;
then
1
- (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ) = 0
by A18, SQUARE_1:92;
then
1
= (((p2 `1 ) / |.p2.|) - cn) / (1 - cn)
by A6, A12, SQUARE_1:83, SQUARE_1:89;
then
1
* (1 - cn) = ((p2 `1 ) / |.p2.|) - cn
by A6, XCMPLX_1:88;
then
1
* |.p2.| = p2 `1
by A9, TOPRNS_1:25, XCMPLX_1:88;
then
p2 `2 = 0
by A13, XCMPLX_1:6;
hence
x1 = x2
by A5, A8, Th120;
verumset p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|;
end; suppose A19:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| < cn &
p2 `2 <= 0 )
;
x1 = x2then A20:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|
by A1, A2, Th122;
then A21:
p1 `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))))
by A5, A8, EUCLID:56;
A22:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
A23:
|.p2.| <> 0
by A19, TOPRNS_1:25;
then A24:
|.p2.| ^2 > 0
by SQUARE_1:74;
A25:
1
+ cn > 0
by A1, XREAL_1:150;
A26:
((p2 `1 ) / |.p2.|) - cn <= 0
by A19, XREAL_1:49;
then A27:
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by A25;
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by XREAL_1:9;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by A22, XREAL_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A24, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
(- ((p2 `1 ) / |.p2.|)) ^2 <= 1
;
then
1
>= - ((p2 `1 ) / |.p2.|)
by SQUARE_1:121;
then
1
+ cn >= (- ((p2 `1 ) / |.p2.|)) + cn
by XREAL_1:9;
then
(- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn) <= 1
by A25, XREAL_1:187;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A27, SQUARE_1:119;
then A28:
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 )) >= 0
by SQUARE_1:def 4;
then
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) ^2 ) / ((1 + cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) ^2 ) / ((1 + cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
p1 `2 = 0
by A5, A7, A8, A20, EUCLID:56;
then A29:
- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))) = - 0
by A21, A23, XCMPLX_1:6;
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))) ^2 ) >= 0
by A28, XCMPLX_1:188;
then
1
- (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ) = 0
by A29, SQUARE_1:92;
then
1
= (- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))) ^2
;
then
1
= - ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))
by A25, A26, SQUARE_1:83, SQUARE_1:89;
then
1
= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by XCMPLX_1:188;
then
1
* (1 + cn) = - (((p2 `1 ) / |.p2.|) - cn)
by A25, XCMPLX_1:88;
then
(1 + cn) - cn = - ((p2 `1 ) / |.p2.|)
;
then
1
= (- (p2 `1 )) / |.p2.|
by XCMPLX_1:188;
then
1
* |.p2.| = - (p2 `1 )
by A19, TOPRNS_1:25, XCMPLX_1:88;
then
((p2 `1 ) ^2 ) - ((p2 `1 ) ^2 ) = (p2 `2 ) ^2
by A22, XCMPLX_1:26;
then
p2 `2 = 0
by XCMPLX_1:6;
hence
x1 = x2
by A5, A8, Th120;
verumset p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|;
end; end; suppose A30:
(
(p1 `1 ) / |.p1.| >= cn &
p1 `2 <= 0 &
p1 <> 0. (TOP-REAL 2) )
;
x1 = x2then
|.p1.| <> 0
by TOPRNS_1:25;
then A31:
|.p1.| ^2 > 0
by SQUARE_1:74;
set q4 =
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|;
A32:
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))
by EUCLID:56;
A33:
(cn -FanMorphS ) . p1 = |[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|
by A1, A2, A30, Th122;
per cases
( p2 `2 >= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| >= cn & p2 `2 <= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| < cn & p2 `2 <= 0 ) )
by JGRAPH_2:11;
suppose A34:
p2 `2 >= 0
;
x1 = x2then A35:
(cn -FanMorphS ) . p2 = p2
by Th120;
then A36:
p2 `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))))
by A5, A33, EUCLID:56;
A37:
((p1 `1 ) / |.p1.|) - cn >= 0
by A30, XREAL_1:50;
A38:
1
- cn > 0
by A2, XREAL_1:151;
A39:
|.p1.| <> 0
by A30, TOPRNS_1:25;
then A40:
|.p1.| ^2 > 0
by SQUARE_1:74;
A41:
((p1 `1 ) / |.p1.|) - cn >= 0
by A30, XREAL_1:50;
A42:
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by A42, XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A40, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p1 `1 ) / |.p1.|
by SQUARE_1:121;
then
1
- cn >= ((p1 `1 ) / |.p1.|) - cn
by XREAL_1:11;
then
- (1 - cn) <= - (((p1 `1 ) / |.p1.|) - cn)
by XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A38, XREAL_1:74;
then
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A38, XCMPLX_1:198;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A38, A41, SQUARE_1:119;
then A43:
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 )) >= 0
by SQUARE_1:def 4;
then
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) ^2 ) / ((1 - cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) ^2 ) / ((1 - cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
p2 `2 = 0
by A5, A33, A34, A35, EUCLID:56;
then A44:
- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))) = - 0
by A36, A39, XCMPLX_1:6;
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))) ^2 ) >= 0
by A43, XCMPLX_1:188;
then
1
- (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ) = 0
by A44, SQUARE_1:92;
then
1
= (((p1 `1 ) / |.p1.|) - cn) / (1 - cn)
by A38, A37, SQUARE_1:83, SQUARE_1:89;
then
1
* (1 - cn) = ((p1 `1 ) / |.p1.|) - cn
by A38, XCMPLX_1:88;
then
1
* |.p1.| = p1 `1
by A30, TOPRNS_1:25, XCMPLX_1:88;
then
p1 `2 = 0
by A42, XCMPLX_1:6;
hence
x1 = x2
by A5, A35, Th120;
verum end; suppose A45:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| >= cn &
p2 `2 <= 0 )
;
x1 = x2
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
(
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) &
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) )
by JGRAPH_3:10, XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A31, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p1 `1 ) / |.p1.|
by SQUARE_1:121;
then
1
- cn >= ((p1 `1 ) / |.p1.|) - cn
by XREAL_1:11;
then
- (1 - cn) <= - (((p1 `1 ) / |.p1.|) - cn)
by XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A6, XREAL_1:74;
then A46:
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A6, XCMPLX_1:198;
((p1 `1 ) / |.p1.|) - cn >= 0
by A30, XREAL_1:50;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A6, A46, SQUARE_1:119;
then
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then A47:
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))) ^2 ) >= 0
by XCMPLX_1:188;
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))))
by EUCLID:56;
then A48:
(|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 =
(|.p1.| ^2 ) * ((sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))) ^2 )
.=
(|.p1.| ^2 ) * (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))
by A47, SQUARE_1:def 4
;
A49:
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))
by EUCLID:56;
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 =
((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p1.| ^2
by A49, A48
;
then A50:
sqrt (|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 ) = |.p1.|
by SQUARE_1:89;
then A51:
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|.| = |.p1.|
by SQUARE_1:89;
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
(
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) &
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) )
by JGRAPH_3:10, XREAL_1:9;
then A52:
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by XREAL_1:74;
|.p2.| <> 0
by A45, TOPRNS_1:25;
then
|.p2.| ^2 > 0
by SQUARE_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A52, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p2 `1 ) / |.p2.|
by SQUARE_1:121;
then
1
- cn >= ((p2 `1 ) / |.p2.|) - cn
by XREAL_1:11;
then
- (1 - cn) <= - (((p2 `1 ) / |.p2.|) - cn)
by XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A6, XREAL_1:74;
then A53:
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A6, XCMPLX_1:198;
((p2 `1 ) / |.p2.|) - cn >= 0
by A45, XREAL_1:50;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A6, A53, SQUARE_1:119;
then
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then A54:
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))) ^2 ) >= 0
by XCMPLX_1:188;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|;
A55:
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))
by EUCLID:56;
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))))
by EUCLID:56;
then A56:
(|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 =
(|.p2.| ^2 ) * ((sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))) ^2 )
.=
(|.p2.| ^2 ) * (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))
by A54, SQUARE_1:def 4
;
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 =
((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p2.| ^2
by A55, A56
;
then A57:
sqrt (|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 ) = |.p2.|
by SQUARE_1:89;
then A58:
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|.| = |.p2.|
by SQUARE_1:89;
A59:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|
by A1, A2, A45, Th122;
then
(((p2 `1 ) / |.p2.|) - cn) / (1 - cn) = (|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))) / |.p2.|
by A5, A33, A32, A45, A55, TOPRNS_1:25, XCMPLX_1:90;
then
(((p2 `1 ) / |.p2.|) - cn) / (1 - cn) = (((p1 `1 ) / |.p1.|) - cn) / (1 - cn)
by A5, A33, A45, A59, A50, A57, TOPRNS_1:25, XCMPLX_1:90;
then
((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) * (1 - cn) = ((p1 `1 ) / |.p1.|) - cn
by A6, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) - cn = ((p1 `1 ) / |.p1.|) - cn
by A6, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) * |.p2.| = p1 `1
by A5, A33, A45, A59, A51, A58, TOPRNS_1:25, XCMPLX_1:88;
then A60:
p2 `1 = p1 `1
by A45, TOPRNS_1:25, XCMPLX_1:88;
(
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) &
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) )
by JGRAPH_3:10;
then
(- (p2 `2 )) ^2 = (p1 `2 ) ^2
by A5, A33, A59, A51, A58, A60;
then
- (p2 `2 ) = sqrt ((- (p1 `2 )) ^2 )
by A45, SQUARE_1:89;
then A61:
- (- (p2 `2 )) = - (- (p1 `2 ))
by A30, SQUARE_1:89;
p2 = |[(p2 `1 ),(p2 `2 )]|
by EUCLID:57;
hence
x1 = x2
by A60, A61, EUCLID:57;
verum end; suppose A62:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| < cn &
p2 `2 <= 0 )
;
x1 = x2then
((p2 `1 ) / |.p2.|) - cn < 0
by XREAL_1:51;
then A63:
(((p2 `1 ) / |.p2.|) - cn) / (1 + cn) < 0
by A1, XREAL_1:143, XREAL_1:150;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|;
A64:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) &
((p1 `1 ) / |.p1.|) - cn >= 0 )
by A30, EUCLID:56, XREAL_1:50;
A65:
1
- cn > 0
by A2, XREAL_1:151;
(
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| &
|.p2.| <> 0 )
by A1, A2, A62, Th122, TOPRNS_1:25;
hence
x1 = x2
by A5, A33, A32, A63, A64, A65, XREAL_1:134;
verum end; end; suppose A66:
(
(p1 `1 ) / |.p1.| < cn &
p1 `2 <= 0 &
p1 <> 0. (TOP-REAL 2) )
;
x1 = x2then A67:
|.p1.| <> 0
by TOPRNS_1:25;
then A68:
|.p1.| ^2 > 0
by SQUARE_1:74;
set q4 =
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|;
A69:
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))
by EUCLID:56;
A70:
(cn -FanMorphS ) . p1 = |[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|
by A1, A2, A66, Th122;
per cases
( p2 `2 >= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| >= cn & p2 `2 <= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| < cn & p2 `2 <= 0 ) )
by JGRAPH_2:11;
suppose A71:
p2 `2 >= 0
;
x1 = x2then A72:
(cn -FanMorphS ) . p2 = p2
by Th120;
then A73:
p2 `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))))
by A5, A70, EUCLID:56;
A74:
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
A75:
1
+ cn > 0
by A1, XREAL_1:150;
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by A74, XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A68, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
(- ((p1 `1 ) / |.p1.|)) ^2 <= 1
;
then
1
>= - ((p1 `1 ) / |.p1.|)
by SQUARE_1:121;
then
1
+ cn >= (- ((p1 `1 ) / |.p1.|)) + cn
by XREAL_1:9;
then A76:
(- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn) <= 1
by A75, XREAL_1:187;
A77:
((p1 `1 ) / |.p1.|) - cn <= 0
by A66, XREAL_1:49;
then
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by A75;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A76, SQUARE_1:119;
then A78:
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then A79:
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) ^2 ) >= 0
by XCMPLX_1:188;
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 )) >= 0
by A78, SQUARE_1:def 4;
then
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) ^2 ) / ((1 + cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) ^2 ) / ((1 + cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
p2 `2 = 0
by A5, A70, A71, A72, EUCLID:56;
then
- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))) = - 0
by A67, A73, XCMPLX_1:6;
then
1
- (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ) = 0
by A79, SQUARE_1:92;
then
1
= (- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) ^2
;
then
1
= - ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))
by A75, A77, SQUARE_1:83, SQUARE_1:89;
then
1
= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by XCMPLX_1:188;
then
1
* (1 + cn) = - (((p1 `1 ) / |.p1.|) - cn)
by A75, XCMPLX_1:88;
then
(1 + cn) - cn = - ((p1 `1 ) / |.p1.|)
;
then
1
= (- (p1 `1 )) / |.p1.|
by XCMPLX_1:188;
then
1
* |.p1.| = - (p1 `1 )
by A66, TOPRNS_1:25, XCMPLX_1:88;
then
((p1 `1 ) ^2 ) - ((p1 `1 ) ^2 ) = (p1 `2 ) ^2
by A74, XCMPLX_1:26;
then
p1 `2 = 0
by XCMPLX_1:6;
hence
x1 = x2
by A5, A72, Th120;
verum end; suppose A80:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| >= cn &
p2 `2 <= 0 )
;
x1 = x2set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|;
A81:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) &
|.p1.| <> 0 )
by A66, EUCLID:56, TOPRNS_1:25;
((p1 `1 ) / |.p1.|) - cn < 0
by A66, XREAL_1:51;
then A82:
(((p1 `1 ) / |.p1.|) - cn) / (1 + cn) < 0
by A1, XREAL_1:143, XREAL_1:150;
A83:
1
- cn > 0
by A2, XREAL_1:151;
(
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| &
((p2 `1 ) / |.p2.|) - cn >= 0 )
by A1, A2, A80, Th122, XREAL_1:50;
hence
x1 = x2
by A5, A70, A69, A82, A81, A83, XREAL_1:134;
verum end; suppose A84:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| < cn &
p2 `2 <= 0 )
;
x1 = x2
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
(
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) &
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) )
by JGRAPH_3:10, XREAL_1:9;
then A85:
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by XREAL_1:74;
A86:
1
+ cn > 0
by A1, XREAL_1:150;
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
(
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) &
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) )
by JGRAPH_3:10, XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A68, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
- 1
<= (p1 `1 ) / |.p1.|
by SQUARE_1:121;
then
(- 1) - cn <= ((p1 `1 ) / |.p1.|) - cn
by XREAL_1:11;
then
- ((- 1) - cn) >= - (((p1 `1 ) / |.p1.|) - cn)
by XREAL_1:26;
then A87:
(- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn) <= 1
by A86, XREAL_1:187;
((p1 `1 ) / |.p1.|) - cn <= 0
by A66, XREAL_1:49;
then
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by A86;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A87, SQUARE_1:119;
then
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then A88:
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) ^2 ) >= 0
by XCMPLX_1:188;
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))))
by EUCLID:56;
then A89:
(|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 =
(|.p1.| ^2 ) * ((sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))) ^2 )
.=
(|.p1.| ^2 ) * (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))
by A88, SQUARE_1:def 4
;
A90:
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))
by EUCLID:56;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|;
A91:
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))
by EUCLID:56;
|.p2.| <> 0
by A84, TOPRNS_1:25;
then
|.p2.| ^2 > 0
by SQUARE_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A85, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
- 1
<= (p2 `1 ) / |.p2.|
by SQUARE_1:121;
then
(- 1) - cn <= ((p2 `1 ) / |.p2.|) - cn
by XREAL_1:11;
then
- ((- 1) - cn) >= - (((p2 `1 ) / |.p2.|) - cn)
by XREAL_1:26;
then A92:
(- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn) <= 1
by A86, XREAL_1:187;
((p2 `1 ) / |.p2.|) - cn <= 0
by A84, XREAL_1:49;
then
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by A86;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A92, SQUARE_1:119;
then
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then A93:
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))) ^2 ) >= 0
by XCMPLX_1:188;
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))))
by EUCLID:56;
then A94:
(|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 =
(|.p2.| ^2 ) * ((sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))) ^2 )
.=
(|.p2.| ^2 ) * (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))
by A93, SQUARE_1:def 4
;
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 =
((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p2.| ^2
by A91, A94
;
then A95:
sqrt (|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 ) = |.p2.|
by SQUARE_1:89;
then A96:
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|.| = |.p2.|
by SQUARE_1:89;
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 =
((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p1.| ^2
by A90, A89
;
then A97:
sqrt (|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 ) = |.p1.|
by SQUARE_1:89;
then A98:
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|.| = |.p1.|
by SQUARE_1:89;
A99:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|
by A1, A2, A84, Th122;
then
(((p2 `1 ) / |.p2.|) - cn) / (1 + cn) = (|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) / |.p2.|
by A5, A70, A69, A84, A91, TOPRNS_1:25, XCMPLX_1:90;
then
(((p2 `1 ) / |.p2.|) - cn) / (1 + cn) = (((p1 `1 ) / |.p1.|) - cn) / (1 + cn)
by A5, A70, A84, A99, A97, A95, TOPRNS_1:25, XCMPLX_1:90;
then
((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) * (1 + cn) = ((p1 `1 ) / |.p1.|) - cn
by A86, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) - cn = ((p1 `1 ) / |.p1.|) - cn
by A86, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) * |.p2.| = p1 `1
by A5, A70, A84, A99, A98, A96, TOPRNS_1:25, XCMPLX_1:88;
then A100:
p2 `1 = p1 `1
by A84, TOPRNS_1:25, XCMPLX_1:88;
(
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) &
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) )
by JGRAPH_3:10;
then
(- (p2 `2 )) ^2 = (p1 `2 ) ^2
by A5, A70, A99, A98, A96, A100;
then
- (p2 `2 ) = sqrt ((- (p1 `2 )) ^2 )
by A84, SQUARE_1:89;
then A101:
- (- (p2 `2 )) = - (- (p1 `2 ))
by A66, SQUARE_1:89;
p2 = |[(p2 `1 ),(p2 `2 )]|
by EUCLID:57;
hence
x1 = x2
by A100, A101, EUCLID:57;
verum end; end;
end;
hence
cn -FanMorphS is one-to-one
by FUNCT_1:def 8; verum