let cn be Real; ( - 1 < cn & cn < 1 implies cn -FanMorphN is one-to-one )
assume that
A1:
- 1 < cn
and
A2:
cn < 1
; cn -FanMorphN is one-to-one
for x1, x2 being object st x1 in dom (cn -FanMorphN) & x2 in dom (cn -FanMorphN) & (cn -FanMorphN) . x1 = (cn -FanMorphN) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom (cn -FanMorphN) & x2 in dom (cn -FanMorphN) & (cn -FanMorphN) . x1 = (cn -FanMorphN) . x2 implies x1 = x2 )
assume that A3:
x1 in dom (cn -FanMorphN)
and A4:
x2 in dom (cn -FanMorphN)
and A5:
(cn -FanMorphN) . x1 = (cn -FanMorphN) . 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:149;
now ( ( p1 `2 <= 0 & x1 = x2 ) or ( (p1 `1) / |.p1.| >= cn & p1 `2 >= 0 & p1 <> 0. (TOP-REAL 2) & x1 = x2 ) or ( (p1 `1) / |.p1.| < cn & p1 `2 >= 0 & p1 <> 0. (TOP-REAL 2) & x1 = x2 ) )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:3;
case A7:
p1 `2 <= 0
;
x1 = x2then A8:
(cn -FanMorphN) . p1 = p1
by Th49;
now ( ( p2 `2 <= 0 & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| >= cn & p2 `2 >= 0 & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| < cn & p2 `2 >= 0 & x1 = x2 ) )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:3;
case A9:
(
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))))]|;
A10:
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2)
by JGRAPH_3:1;
0 <= (p2 `2) ^2
by XREAL_1:63;
then
0 + ((p2 `1) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2)
by XREAL_1:7;
then A11:
((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2)
by A10, XREAL_1:72;
A12:
|.p2.| > 0
by A9, Lm1;
then
|.p2.| ^2 > 0
by SQUARE_1:12;
then
((p2 `1) ^2) / (|.p2.| ^2) <= 1
by A11, XCMPLX_1:60;
then
((p2 `1) / |.p2.|) ^2 <= 1
by XCMPLX_1:76;
then
1
>= (p2 `1) / |.p2.|
by SQUARE_1:51;
then
1
- cn >= ((p2 `1) / |.p2.|) - cn
by XREAL_1:9;
then
- (1 - cn) <= - (((p2 `1) / |.p2.|) - cn)
by XREAL_1:24;
then
(- (1 - cn)) / (1 - cn) <= (- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)
by A6, XREAL_1:72;
then A13:
- 1
<= (- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)
by A6, XCMPLX_1:197;
A14:
((p2 `1) / |.p2.|) - cn >= 0
by A9, XREAL_1:48;
A15:
(cn -FanMorphN) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2))))]|
by A1, A2, A9, Th51;
((p2 `1) / |.p2.|) - cn >= 0
by A9, XREAL_1:48;
then
((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A6, A13, SQUARE_1:49;
then A16:
1
- (((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2) >= 0
by XREAL_1:48;
then
sqrt (1 - (((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2)) >= 0
by SQUARE_1:def 2;
then
sqrt (1 - (((- (((p2 `1) / |.p2.|) - cn)) ^2) / ((1 - cn) ^2))) >= 0
by XCMPLX_1:76;
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:76;
then
(
|[(|.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))) &
p1 `2 = 0 )
by A5, A7, A8, A15, EUCLID:52;
then A17:
sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)) = 0
by A5, A8, A15, A12, XCMPLX_1:6;
1
- ((- ((((p2 `1) / |.p2.|) - cn) / (1 - cn))) ^2) >= 0
by A16, XCMPLX_1:187;
then
1
- (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2) = 0
by A17, SQUARE_1:24;
then
1
= (((p2 `1) / |.p2.|) - cn) / (1 - cn)
by A6, A14, SQUARE_1:18, SQUARE_1:22;
then
1
* (1 - cn) = ((p2 `1) / |.p2.|) - cn
by A6, XCMPLX_1:87;
then
1
* |.p2.| = p2 `1
by A12, XCMPLX_1:87;
then
p2 `2 = 0
by A10, XCMPLX_1:6;
hence
x1 = x2
by A5, A8, Th49;
verum end; case A18:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1) / |.p2.| < cn &
p2 `2 >= 0 )
;
x1 = x2then A19:
|.p2.| <> 0
by TOPRNS_1:24;
then A20:
|.p2.| ^2 > 0
by SQUARE_1:12;
set p4 =
|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]|;
A21:
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2)
by JGRAPH_3:1;
A22:
1
+ cn > 0
by A1, XREAL_1:148;
A23:
((p2 `1) / |.p2.|) - cn <= 0
by A18, XREAL_1:47;
then A24:
- 1
<= (- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)
by A22;
A25:
(cn -FanMorphN) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]|
by A1, A2, A18, Th51;
0 <= (p2 `2) ^2
by XREAL_1:63;
then
0 + ((p2 `1) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2)
by XREAL_1:7;
then
((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2)
by A21, XREAL_1:72;
then
((p2 `1) ^2) / (|.p2.| ^2) <= 1
by A20, XCMPLX_1:60;
then
((p2 `1) / |.p2.|) ^2 <= 1
by XCMPLX_1:76;
then
(- ((p2 `1) / |.p2.|)) ^2 <= 1
;
then
1
>= - ((p2 `1) / |.p2.|)
by SQUARE_1:51;
then
1
+ cn >= (- ((p2 `1) / |.p2.|)) + cn
by XREAL_1:7;
then
(- (((p2 `1) / |.p2.|) - cn)) / (1 + cn) <= 1
by A22, XREAL_1:185;
then
((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A24, SQUARE_1:49;
then A26:
1
- (((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2) >= 0
by XREAL_1:48;
then
sqrt (1 - (((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2)) >= 0
by SQUARE_1:def 2;
then
sqrt (1 - (((- (((p2 `1) / |.p2.|) - cn)) ^2) / ((1 + cn) ^2))) >= 0
by XCMPLX_1:76;
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:76;
then
(
|[(|.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))) &
p1 `2 = 0 )
by A5, A7, A8, A25, EUCLID:52;
then A27:
sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)) = 0
by A5, A8, A25, A19, XCMPLX_1:6;
1
- ((- ((((p2 `1) / |.p2.|) - cn) / (1 + cn))) ^2) >= 0
by A26, XCMPLX_1:187;
then
1
- (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2) = 0
by A27, SQUARE_1:24;
then
1
= sqrt ((- ((((p2 `1) / |.p2.|) - cn) / (1 + cn))) ^2)
by SQUARE_1:18;
then
1
= - ((((p2 `1) / |.p2.|) - cn) / (1 + cn))
by A22, A23, SQUARE_1:22;
then
1
= (- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)
by XCMPLX_1:187;
then
1
* (1 + cn) = - (((p2 `1) / |.p2.|) - cn)
by A22, XCMPLX_1:87;
then
(1 + cn) - cn = - ((p2 `1) / |.p2.|)
;
then
1
= (- (p2 `1)) / |.p2.|
by XCMPLX_1:187;
then
1
* |.p2.| = - (p2 `1)
by A18, TOPRNS_1:24, XCMPLX_1:87;
then
((p2 `1) ^2) - ((p2 `1) ^2) = (p2 `2) ^2
by A21, XCMPLX_1:26;
then
p2 `2 = 0
by XCMPLX_1:6;
hence
x1 = x2
by A5, A8, Th49;
verum end; end; end; hence
x1 = x2
;
verum end; case A28:
(
(p1 `1) / |.p1.| >= cn &
p1 `2 >= 0 &
p1 <> 0. (TOP-REAL 2) )
;
x1 = x2then
|.p1.| <> 0
by TOPRNS_1:24;
then A29:
|.p1.| ^2 > 0
by SQUARE_1:12;
set q4 =
|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2))))]|;
A30:
|[(|.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:52;
A31:
(cn -FanMorphN) . p1 = |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2))))]|
by A1, A2, A28, Th51;
A32:
|[(|.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:52;
now ( ( p2 `2 <= 0 & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| >= cn & p2 `2 >= 0 & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| < cn & p2 `2 >= 0 & x1 = x2 ) )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:3;
case A33:
p2 `2 <= 0
;
x1 = x2then A34:
(cn -FanMorphN) . p2 = p2
by Th49;
A35:
|.p1.| <> 0
by A28, TOPRNS_1:24;
then A36:
|.p1.| ^2 > 0
by SQUARE_1:12;
A37:
((p1 `1) / |.p1.|) - cn >= 0
by A28, XREAL_1:48;
A38:
|.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by JGRAPH_3:1;
A39:
((p1 `1) / |.p1.|) - cn >= 0
by A28, XREAL_1:48;
A40:
1
- cn > 0
by A2, XREAL_1:149;
0 <= (p1 `2) ^2
by XREAL_1:63;
then
0 + ((p1 `1) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2)
by XREAL_1:7;
then
((p1 `1) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2)
by A38, XREAL_1:72;
then
((p1 `1) ^2) / (|.p1.| ^2) <= 1
by A36, XCMPLX_1:60;
then
((p1 `1) / |.p1.|) ^2 <= 1
by XCMPLX_1:76;
then
1
>= (p1 `1) / |.p1.|
by SQUARE_1:51;
then
1
- cn >= ((p1 `1) / |.p1.|) - cn
by XREAL_1:9;
then
- (1 - cn) <= - (((p1 `1) / |.p1.|) - cn)
by XREAL_1:24;
then
(- (1 - cn)) / (1 - cn) <= (- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)
by A40, XREAL_1:72;
then
- 1
<= (- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)
by A40, XCMPLX_1:197;
then
((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A40, A37, SQUARE_1:49;
then A41:
1
- (((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2) >= 0
by XREAL_1:48;
then
sqrt (1 - (((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2)) >= 0
by SQUARE_1:def 2;
then
sqrt (1 - (((- (((p1 `1) / |.p1.|) - cn)) ^2) / ((1 - cn) ^2))) >= 0
by XCMPLX_1:76;
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:76;
then
p2 `2 = 0
by A5, A31, A33, A34, EUCLID:52;
then A42:
sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)) = 0
by A5, A31, A32, A34, A35, XCMPLX_1:6;
1
- ((- ((((p1 `1) / |.p1.|) - cn) / (1 - cn))) ^2) >= 0
by A41, XCMPLX_1:187;
then
1
- (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2) = 0
by A42, SQUARE_1:24;
then
1
= (((p1 `1) / |.p1.|) - cn) / (1 - cn)
by A40, A39, SQUARE_1:18, SQUARE_1:22;
then
1
* (1 - cn) = ((p1 `1) / |.p1.|) - cn
by A40, XCMPLX_1:87;
then
1
* |.p1.| = p1 `1
by A28, TOPRNS_1:24, XCMPLX_1:87;
then
p1 `2 = 0
by A38, XCMPLX_1:6;
hence
x1 = x2
by A5, A34, Th49;
verum end; case A43:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1) / |.p2.| >= cn &
p2 `2 >= 0 )
;
x1 = x2
0 <= (p1 `2) ^2
by XREAL_1:63;
then
(
|.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) &
0 + ((p1 `1) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then
((p1 `1) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2)
by XREAL_1:72;
then
((p1 `1) ^2) / (|.p1.| ^2) <= 1
by A29, XCMPLX_1:60;
then
((p1 `1) / |.p1.|) ^2 <= 1
by XCMPLX_1:76;
then
1
>= (p1 `1) / |.p1.|
by SQUARE_1:51;
then
1
- cn >= ((p1 `1) / |.p1.|) - cn
by XREAL_1:9;
then
- (1 - cn) <= - (((p1 `1) / |.p1.|) - cn)
by XREAL_1:24;
then
(- (1 - cn)) / (1 - cn) <= (- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)
by A6, XREAL_1:72;
then A44:
- 1
<= (- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)
by A6, XCMPLX_1:197;
((p1 `1) / |.p1.|) - cn >= 0
by A28, XREAL_1:48;
then
((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A6, A44, SQUARE_1:49;
then
1
- (((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2) >= 0
by XREAL_1:48;
then A45:
1
- ((- ((((p1 `1) / |.p1.|) - cn) / (1 - cn))) ^2) >= 0
by XCMPLX_1:187;
|[(|.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:52;
then A46:
(|[(|.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 A45, SQUARE_1:def 2
;
A47:
|[(|.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:52;
|.|[(|.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:1
.=
|.p1.| ^2
by A47, A46
;
then A48:
sqrt (|.|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2))))]|.| ^2) = |.p1.|
by SQUARE_1:22;
then A49:
|.|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2))))]|.| = |.p1.|
by SQUARE_1:22;
0 <= (p2 `2) ^2
by XREAL_1:63;
then
(
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) &
0 + ((p2 `1) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then A50:
((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2)
by XREAL_1:72;
|.p2.| <> 0
by A43, TOPRNS_1:24;
then
|.p2.| ^2 > 0
by SQUARE_1:12;
then
((p2 `1) ^2) / (|.p2.| ^2) <= 1
by A50, XCMPLX_1:60;
then
((p2 `1) / |.p2.|) ^2 <= 1
by XCMPLX_1:76;
then
1
>= (p2 `1) / |.p2.|
by SQUARE_1:51;
then
1
- cn >= ((p2 `1) / |.p2.|) - cn
by XREAL_1:9;
then
- (1 - cn) <= - (((p2 `1) / |.p2.|) - cn)
by XREAL_1:24;
then
(- (1 - cn)) / (1 - cn) <= (- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)
by A6, XREAL_1:72;
then A51:
- 1
<= (- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)
by A6, XCMPLX_1:197;
((p2 `1) / |.p2.|) - cn >= 0
by A43, XREAL_1:48;
then
((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A6, A51, SQUARE_1:49;
then
1
- (((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2) >= 0
by XREAL_1:48;
then A52:
1
- ((- ((((p2 `1) / |.p2.|) - cn) / (1 - cn))) ^2) >= 0
by XCMPLX_1:187;
set p4 =
|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2))))]|;
A53:
|[(|.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:52;
|[(|.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:52;
then A54:
(|[(|.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 A52, SQUARE_1:def 2
;
|.|[(|.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:1
.=
|.p2.| ^2
by A53, A54
;
then A55:
sqrt (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2))))]|.| ^2) = |.p2.|
by SQUARE_1:22;
then A56:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2))))]|.| = |.p2.|
by SQUARE_1:22;
A57:
(cn -FanMorphN) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2))))]|
by A1, A2, A43, Th51;
then
(((p2 `1) / |.p2.|) - cn) / (1 - cn) = (|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))) / |.p2.|
by A5, A31, A30, A43, A53, TOPRNS_1:24, XCMPLX_1:89;
then
(((p2 `1) / |.p2.|) - cn) / (1 - cn) = (((p1 `1) / |.p1.|) - cn) / (1 - cn)
by A5, A31, A43, A57, A48, A55, TOPRNS_1:24, XCMPLX_1:89;
then
((((p2 `1) / |.p2.|) - cn) / (1 - cn)) * (1 - cn) = ((p1 `1) / |.p1.|) - cn
by A6, XCMPLX_1:87;
then
((p2 `1) / |.p2.|) - cn = ((p1 `1) / |.p1.|) - cn
by A6, XCMPLX_1:87;
then
((p2 `1) / |.p2.|) * |.p2.| = p1 `1
by A5, A31, A43, A57, A49, A56, TOPRNS_1:24, XCMPLX_1:87;
then A58:
p2 `1 = p1 `1
by A43, TOPRNS_1:24, XCMPLX_1:87;
A59:
p2 = |[(p2 `1),(p2 `2)]|
by EUCLID:53;
(
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) &
|.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) )
by JGRAPH_3:1;
then
p2 `2 = sqrt ((p1 `2) ^2)
by A5, A31, A43, A57, A49, A56, A58, SQUARE_1:22;
then
p2 `2 = p1 `2
by A28, SQUARE_1:22;
hence
x1 = x2
by A58, A59, EUCLID:53;
verum end; case A60:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1) / |.p2.| < cn &
p2 `2 >= 0 )
;
x1 = x2then
((p2 `1) / |.p2.|) - cn < 0
by XREAL_1:49;
then A61:
(((p2 `1) / |.p2.|) - cn) / (1 + cn) < 0
by A1, XREAL_1:141, XREAL_1:148;
set p4 =
|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]|;
A62:
(
|[(|.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 A28, EUCLID:52, XREAL_1:48;
A63:
1
- cn > 0
by A2, XREAL_1:149;
(
(cn -FanMorphN) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]| &
|.p2.| <> 0 )
by A1, A2, A60, Th51, TOPRNS_1:24;
hence
x1 = x2
by A5, A31, A30, A61, A62, A63, XREAL_1:132;
verum end; end; end; hence
x1 = x2
;
verum end; case A64:
(
(p1 `1) / |.p1.| < cn &
p1 `2 >= 0 &
p1 <> 0. (TOP-REAL 2) )
;
x1 = x2then A65:
|.p1.| <> 0
by TOPRNS_1:24;
then A66:
|.p1.| ^2 > 0
by SQUARE_1:12;
set q4 =
|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2))))]|;
A67:
|[(|.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:52;
A68:
(cn -FanMorphN) . p1 = |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2))))]|
by A1, A2, A64, Th51;
A69:
|[(|.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:52;
now ( ( p2 `2 <= 0 & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| >= cn & p2 `2 >= 0 & x1 = x2 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| < cn & p2 `2 >= 0 & x1 = x2 ) )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:3;
case A70:
p2 `2 <= 0
;
x1 = x2A71:
|.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by JGRAPH_3:1;
A72:
1
+ cn > 0
by A1, XREAL_1:148;
0 <= (p1 `2) ^2
by XREAL_1:63;
then
0 + ((p1 `1) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2)
by XREAL_1:7;
then
((p1 `1) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2)
by A71, XREAL_1:72;
then
((p1 `1) ^2) / (|.p1.| ^2) <= 1
by A66, XCMPLX_1:60;
then
((p1 `1) / |.p1.|) ^2 <= 1
by XCMPLX_1:76;
then
(- ((p1 `1) / |.p1.|)) ^2 <= 1
;
then
1
>= - ((p1 `1) / |.p1.|)
by SQUARE_1:51;
then
1
+ cn >= (- ((p1 `1) / |.p1.|)) + cn
by XREAL_1:7;
then A73:
(- (((p1 `1) / |.p1.|) - cn)) / (1 + cn) <= 1
by A72, XREAL_1:185;
A74:
((p1 `1) / |.p1.|) - cn <= 0
by A64, XREAL_1:47;
then
- 1
<= (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)
by A72;
then
((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A73, SQUARE_1:49;
then A75:
1
- (((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2) >= 0
by XREAL_1:48;
then A76:
1
- ((- ((((p1 `1) / |.p1.|) - cn) / (1 + cn))) ^2) >= 0
by XCMPLX_1:187;
A77:
(cn -FanMorphN) . p2 = p2
by A70, Th49;
sqrt (1 - (((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2)) >= 0
by A75, SQUARE_1:def 2;
then
sqrt (1 - (((- (((p1 `1) / |.p1.|) - cn)) ^2) / ((1 + cn) ^2))) >= 0
by XCMPLX_1:76;
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:76;
then
p2 `2 = 0
by A5, A68, A70, A77, EUCLID:52;
then
sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)) = 0
by A5, A68, A69, A65, A77, XCMPLX_1:6;
then
1
- (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2) = 0
by A76, SQUARE_1:24;
then
1
= sqrt ((- ((((p1 `1) / |.p1.|) - cn) / (1 + cn))) ^2)
by SQUARE_1:18;
then
1
= - ((((p1 `1) / |.p1.|) - cn) / (1 + cn))
by A72, A74, SQUARE_1:22;
then
1
= (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)
by XCMPLX_1:187;
then
1
* (1 + cn) = - (((p1 `1) / |.p1.|) - cn)
by A72, XCMPLX_1:87;
then
(1 + cn) - cn = - ((p1 `1) / |.p1.|)
;
then
1
= (- (p1 `1)) / |.p1.|
by XCMPLX_1:187;
then
1
* |.p1.| = - (p1 `1)
by A64, TOPRNS_1:24, XCMPLX_1:87;
then
((p1 `1) ^2) - ((p1 `1) ^2) = (p1 `2) ^2
by A71, XCMPLX_1:26;
then
p1 `2 = 0
by XCMPLX_1:6;
hence
x1 = x2
by A5, A77, Th49;
verum end; case A78:
(
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))))]|;
A79:
(
|[(|.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 A64, EUCLID:52, TOPRNS_1:24;
((p1 `1) / |.p1.|) - cn < 0
by A64, XREAL_1:49;
then A80:
(((p1 `1) / |.p1.|) - cn) / (1 + cn) < 0
by A1, XREAL_1:141, XREAL_1:148;
A81:
1
- cn > 0
by A2, XREAL_1:149;
(
(cn -FanMorphN) . 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, A78, Th51, XREAL_1:48;
hence
x1 = x2
by A5, A68, A67, A80, A79, A81, XREAL_1:132;
verum end; case A82:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1) / |.p2.| < cn &
p2 `2 >= 0 )
;
x1 = x2
0 <= (p2 `2) ^2
by XREAL_1:63;
then
(
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) &
0 + ((p2 `1) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then A83:
((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2)
by XREAL_1:72;
A84:
1
+ cn > 0
by A1, XREAL_1:148;
0 <= (p1 `2) ^2
by XREAL_1:63;
then
(
|.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) &
0 + ((p1 `1) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then
((p1 `1) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2)
by XREAL_1:72;
then
((p1 `1) ^2) / (|.p1.| ^2) <= 1
by A66, XCMPLX_1:60;
then
((p1 `1) / |.p1.|) ^2 <= 1
by XCMPLX_1:76;
then
- 1
<= (p1 `1) / |.p1.|
by SQUARE_1:51;
then
(- 1) - cn <= ((p1 `1) / |.p1.|) - cn
by XREAL_1:9;
then
- ((- 1) - cn) >= - (((p1 `1) / |.p1.|) - cn)
by XREAL_1:24;
then A85:
(- (((p1 `1) / |.p1.|) - cn)) / (1 + cn) <= 1
by A84, XREAL_1:185;
((p1 `1) / |.p1.|) - cn <= 0
by A64, XREAL_1:47;
then
- 1
<= (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)
by A84;
then
((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A85, SQUARE_1:49;
then
1
- (((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2) >= 0
by XREAL_1:48;
then A86:
1
- ((- ((((p1 `1) / |.p1.|) - cn) / (1 + cn))) ^2) >= 0
by XCMPLX_1:187;
|[(|.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:52;
then A87:
(|[(|.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 A86, SQUARE_1:def 2
;
A88:
|[(|.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:52;
set p4 =
|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]|;
A89:
|[(|.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:52;
|.p2.| <> 0
by A82, TOPRNS_1:24;
then
|.p2.| ^2 > 0
by SQUARE_1:12;
then
((p2 `1) ^2) / (|.p2.| ^2) <= 1
by A83, XCMPLX_1:60;
then
((p2 `1) / |.p2.|) ^2 <= 1
by XCMPLX_1:76;
then
- 1
<= (p2 `1) / |.p2.|
by SQUARE_1:51;
then
(- 1) - cn <= ((p2 `1) / |.p2.|) - cn
by XREAL_1:9;
then
- ((- 1) - cn) >= - (((p2 `1) / |.p2.|) - cn)
by XREAL_1:24;
then A90:
(- (((p2 `1) / |.p2.|) - cn)) / (1 + cn) <= 1
by A84, XREAL_1:185;
((p2 `1) / |.p2.|) - cn <= 0
by A82, XREAL_1:47;
then
- 1
<= (- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)
by A84;
then
((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A90, SQUARE_1:49;
then
1
- (((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2) >= 0
by XREAL_1:48;
then A91:
1
- ((- ((((p2 `1) / |.p2.|) - cn) / (1 + cn))) ^2) >= 0
by XCMPLX_1:187;
|[(|.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:52;
then A92:
(|[(|.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 A91, SQUARE_1:def 2
;
|.|[(|.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:1
.=
|.p2.| ^2
by A89, A92
;
then A93:
sqrt (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]|.| ^2) = |.p2.|
by SQUARE_1:22;
then A94:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]|.| = |.p2.|
by SQUARE_1:22;
|.|[(|.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:1
.=
|.p1.| ^2
by A88, A87
;
then A95:
sqrt (|.|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2))))]|.| ^2) = |.p1.|
by SQUARE_1:22;
then A96:
|.|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2))))]|.| = |.p1.|
by SQUARE_1:22;
A97:
(cn -FanMorphN) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))))]|
by A1, A2, A82, Th51;
then
(((p2 `1) / |.p2.|) - cn) / (1 + cn) = (|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))) / |.p2.|
by A5, A68, A67, A82, A89, TOPRNS_1:24, XCMPLX_1:89;
then
(((p2 `1) / |.p2.|) - cn) / (1 + cn) = (((p1 `1) / |.p1.|) - cn) / (1 + cn)
by A5, A68, A82, A97, A95, A93, TOPRNS_1:24, XCMPLX_1:89;
then
((((p2 `1) / |.p2.|) - cn) / (1 + cn)) * (1 + cn) = ((p1 `1) / |.p1.|) - cn
by A84, XCMPLX_1:87;
then
((p2 `1) / |.p2.|) - cn = ((p1 `1) / |.p1.|) - cn
by A84, XCMPLX_1:87;
then
((p2 `1) / |.p2.|) * |.p2.| = p1 `1
by A5, A68, A82, A97, A96, A94, TOPRNS_1:24, XCMPLX_1:87;
then A98:
p2 `1 = p1 `1
by A82, TOPRNS_1:24, XCMPLX_1:87;
A99:
p2 = |[(p2 `1),(p2 `2)]|
by EUCLID:53;
(
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) &
|.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) )
by JGRAPH_3:1;
then
p2 `2 = sqrt ((p1 `2) ^2)
by A5, A68, A82, A97, A96, A94, A98, SQUARE_1:22;
then
p2 `2 = p1 `2
by A64, SQUARE_1:22;
hence
x1 = x2
by A98, A99, EUCLID:53;
verum end; end; end; hence
x1 = x2
;
verum end; end; end;
hence
x1 = x2
;
verum
end;
hence
cn -FanMorphN is one-to-one
by FUNCT_1:def 4; verum