let sn be Real; :: thesis: ( - 1 < sn & sn < 1 implies sn -FanMorphE is one-to-one )
assume that
A1: - 1 < sn and
A2: sn < 1 ; :: thesis: sn -FanMorphE is one-to-one
for x1, x2 being object st x1 in dom (sn -FanMorphE) & x2 in dom (sn -FanMorphE) & (sn -FanMorphE) . x1 = (sn -FanMorphE) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (sn -FanMorphE) & x2 in dom (sn -FanMorphE) & (sn -FanMorphE) . x1 = (sn -FanMorphE) . x2 implies x1 = x2 )
assume that
A3: x1 in dom (sn -FanMorphE) and
A4: x2 in dom (sn -FanMorphE) and
A5: (sn -FanMorphE) . x1 = (sn -FanMorphE) . x2 ; :: thesis: 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 - sn > 0 by A2, XREAL_1:149;

now :: thesis: ( ( p1 `1 <= 0 & x1 = x2 ) or ( (p1 `2) / |.p1.| >= sn & p1 `1 >= 0 & p1 <> 0. (TOP-REAL 2) & x1 = x2 ) or ( (p1 `2) / |.p1.| < sn & p1 `1 >= 0 & p1 <> 0. (TOP-REAL 2) & x1 = x2 ) )

per cases ( p1 `1 <= 0 or ( (p1 `2) / |.p1.| >= sn & p1 `1 >= 0 & p1 <> 0. (TOP-REAL 2) ) or ( (p1 `2) / |.p1.| < sn & p1 `1 >= 0 & p1 <> 0. (TOP-REAL 2) ) ) by JGRAPH_2:3;

case A7: p1 `1 <= 0 ; :: thesis: x1 = x2

then A8: (sn -FanMorphE) . p1 = p1 by Th82;

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

per cases ( p2 `1 <= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| >= sn & p2 `1 >= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| < sn & p2 `1 >= 0 ) ) by JGRAPH_2:3;

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

hence x1 = x2 by A5, A8, Th82; :: thesis: verum

end;

case A9: ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| >= sn & p2 `1 >= 0 ) ; :: thesis: x1 = x2

then A10: ((p2 `2) / |.p2.|) - sn >= 0 by XREAL_1:48;
set p4 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|;
A11: |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
A12: |.p2.| <> 0 by A9, TOPRNS_1:24;
then A13: |.p2.| ^2 > 0 by SQUARE_1:12;
0 <= (p2 `1) ^2 by XREAL_1:63;
then 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) by XREAL_1:7;
then ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by A11, XREAL_1:72;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A13, XCMPLX_1:60;
then ((p2 `2) / |.p2.|) ^2 <= 1 by XCMPLX_1:76;
then 1 >= (p2 `2) / |.p2.| by SQUARE_1:51;
then 1 - sn >= ((p2 `2) / |.p2.|) - sn by XREAL_1:9;
then - (1 - sn) <= - (((p2 `2) / |.p2.|) - sn) by XREAL_1:24;
then (- (1 - sn)) / (1 - sn) <= (- (((p2 `2) / |.p2.|) - sn)) / (1 - sn) by A6, XREAL_1:72;
then A14: - 1 <= (- (((p2 `2) / |.p2.|) - sn)) / (1 - sn) by A6, XCMPLX_1:197;
A15: (sn -FanMorphE) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| by A1, A2, A9, Th84;
((p2 `2) / |.p2.|) - sn >= 0 by A9, XREAL_1:48;
then ((- (((p2 `2) / |.p2.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A6, A14, SQUARE_1:49;
then A16: 1 - (((- (((p2 `2) / |.p2.|) - sn)) / (1 - sn)) ^2) >= 0 by XREAL_1:48;
then sqrt (1 - (((- (((p2 `2) / |.p2.|) - sn)) / (1 - sn)) ^2)) >= 0 by SQUARE_1:def 2;
then sqrt (1 - (((- (((p2 `2) / |.p2.|) - sn)) ^2) / ((1 - sn) ^2))) >= 0 by XCMPLX_1:76;
then sqrt (1 - (((((p2 `2) / |.p2.|) - sn) ^2) / ((1 - sn) ^2))) >= 0 ;
then sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)) >= 0 by XCMPLX_1:76;
then ( |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| `1 = |.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2))) & p1 `1 = 0 ) by A5, A7, A8, A15, EUCLID:52;
then A17: sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)) = 0 by A5, A8, A15, A12, XCMPLX_1:6;
1 - ((- ((((p2 `2) / |.p2.|) - sn) / (1 - sn))) ^2) >= 0 by A16, XCMPLX_1:187;
then 1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2) = 0 by A17, SQUARE_1:24;
then 1 = (((p2 `2) / |.p2.|) - sn) / (1 - sn) by A6, A10, SQUARE_1:18, SQUARE_1:22;
then 1 * (1 - sn) = ((p2 `2) / |.p2.|) - sn by A6, XCMPLX_1:87;
then 1 * |.p2.| = p2 `2 by A9, TOPRNS_1:24, XCMPLX_1:87;
then p2 `1 = 0 by A11, XCMPLX_1:6;
hence x1 = x2 by A5, A8, Th82; :: thesis: verum

end;

case A18: ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| < sn & p2 `1 >= 0 ) ; :: thesis: x1 = x2

then A19: |.p2.| <> 0 by TOPRNS_1:24;
then A20: |.p2.| ^2 > 0 by SQUARE_1:12;
set p4 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|;
A21: |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
A22: 1 + sn > 0 by A1, XREAL_1:148;
A23: ((p2 `2) / |.p2.|) - sn <= 0 by A18, XREAL_1:47;
then A24: - 1 <= (- (((p2 `2) / |.p2.|) - sn)) / (1 + sn) by A22;
A25: (sn -FanMorphE) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| by A1, A2, A18, Th84;
0 <= (p2 `1) ^2 by XREAL_1:63;
then 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) by XREAL_1:7;
then ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by A21, XREAL_1:72;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A20, XCMPLX_1:60;
then ((p2 `2) / |.p2.|) ^2 <= 1 by XCMPLX_1:76;
then (- ((p2 `2) / |.p2.|)) ^2 <= 1 ;
then 1 >= - ((p2 `2) / |.p2.|) by SQUARE_1:51;
then 1 + sn >= (- ((p2 `2) / |.p2.|)) + sn by XREAL_1:7;
then (- (((p2 `2) / |.p2.|) - sn)) / (1 + sn) <= 1 by A22, XREAL_1:185;
then ((- (((p2 `2) / |.p2.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A24, SQUARE_1:49;
then A26: 1 - (((- (((p2 `2) / |.p2.|) - sn)) / (1 + sn)) ^2) >= 0 by XREAL_1:48;
then sqrt (1 - (((- (((p2 `2) / |.p2.|) - sn)) / (1 + sn)) ^2)) >= 0 by SQUARE_1:def 2;
then sqrt (1 - (((- (((p2 `2) / |.p2.|) - sn)) ^2) / ((1 + sn) ^2))) >= 0 by XCMPLX_1:76;
then sqrt (1 - (((((p2 `2) / |.p2.|) - sn) ^2) / ((1 + sn) ^2))) >= 0 ;
then sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)) >= 0 by XCMPLX_1:76;
then ( |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| `1 = |.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))) & p1 `1 = 0 ) by A5, A7, A8, A25, EUCLID:52;
then A27: sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)) = 0 by A5, A8, A25, A19, XCMPLX_1:6;
1 - ((- ((((p2 `2) / |.p2.|) - sn) / (1 + sn))) ^2) >= 0 by A26, XCMPLX_1:187;
then 1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2) = 0 by A27, SQUARE_1:24;
then 1 = sqrt ((- ((((p2 `2) / |.p2.|) - sn) / (1 + sn))) ^2) ;
then 1 = - ((((p2 `2) / |.p2.|) - sn) / (1 + sn)) by A22, A23, SQUARE_1:22;
then 1 = (- (((p2 `2) / |.p2.|) - sn)) / (1 + sn) by XCMPLX_1:187;
then 1 * (1 + sn) = - (((p2 `2) / |.p2.|) - sn) by A22, XCMPLX_1:87;
then (1 + sn) - sn = - ((p2 `2) / |.p2.|) ;
then 1 = (- (p2 `2)) / |.p2.| by XCMPLX_1:187;
then 1 * |.p2.| = - (p2 `2) by A18, TOPRNS_1:24, XCMPLX_1:87;
then ((p2 `2) ^2) - ((p2 `2) ^2) = (p2 `1) ^2 by A21, XCMPLX_1:26;
then p2 `1 = 0 by XCMPLX_1:6;
hence x1 = x2 by A5, A8, Th82; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case A28: ( (p1 `2) / |.p1.| >= sn & p1 `1 >= 0 & p1 <> 0. (TOP-REAL 2) ) ; :: thesis: x1 = x2

then |.p1.| <> 0 by TOPRNS_1:24;
then A29: |.p1.| ^2 > 0 by SQUARE_1:12;
set q4 = |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]|;
A30: |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| `2 = |.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)) by EUCLID:52;
A31: (sn -FanMorphE) . p1 = |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| by A1, A2, A28, Th84;
A32: |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| `1 = |.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2))) by EUCLID:52;

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

per cases ( p2 `1 <= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| >= sn & p2 `1 >= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| < sn & p2 `1 >= 0 ) ) by JGRAPH_2:3;

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

then A34: (sn -FanMorphE) . p2 = p2 by Th82;
A35: |.p1.| <> 0 by A28, TOPRNS_1:24;
then A36: |.p1.| ^2 > 0 by SQUARE_1:12;
A37: ((p1 `2) / |.p1.|) - sn >= 0 by A28, XREAL_1:48;
A38: |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
A39: ((p1 `2) / |.p1.|) - sn >= 0 by A28, XREAL_1:48;
A40: 1 - sn > 0 by A2, XREAL_1:149;
0 <= (p1 `1) ^2 by XREAL_1:63;
then 0 + ((p1 `2) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2) by XREAL_1:7;
then ((p1 `2) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2) by A38, XREAL_1:72;
then ((p1 `2) ^2) / (|.p1.| ^2) <= 1 by A36, XCMPLX_1:60;
then ((p1 `2) / |.p1.|) ^2 <= 1 by XCMPLX_1:76;
then 1 >= (p1 `2) / |.p1.| by SQUARE_1:51;
then 1 - sn >= ((p1 `2) / |.p1.|) - sn by XREAL_1:9;
then - (1 - sn) <= - (((p1 `2) / |.p1.|) - sn) by XREAL_1:24;
then (- (1 - sn)) / (1 - sn) <= (- (((p1 `2) / |.p1.|) - sn)) / (1 - sn) by A40, XREAL_1:72;
then - 1 <= (- (((p1 `2) / |.p1.|) - sn)) / (1 - sn) by A40, XCMPLX_1:197;
then ((- (((p1 `2) / |.p1.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A40, A37, SQUARE_1:49;
then A41: 1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 - sn)) ^2) >= 0 by XREAL_1:48;
then sqrt (1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 - sn)) ^2)) >= 0 by SQUARE_1:def 2;
then sqrt (1 - (((- (((p1 `2) / |.p1.|) - sn)) ^2) / ((1 - sn) ^2))) >= 0 by XCMPLX_1:76;
then sqrt (1 - (((((p1 `2) / |.p1.|) - sn) ^2) / ((1 - sn) ^2))) >= 0 ;
then sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)) >= 0 by XCMPLX_1:76;
then p2 `1 = 0 by A5, A31, A33, A34, EUCLID:52;
then A42: sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)) = 0 by A5, A31, A32, A34, A35, XCMPLX_1:6;
1 - ((- ((((p1 `2) / |.p1.|) - sn) / (1 - sn))) ^2) >= 0 by A41, XCMPLX_1:187;
then 1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2) = 0 by A42, SQUARE_1:24;
then 1 = (((p1 `2) / |.p1.|) - sn) / (1 - sn) by A40, A39, SQUARE_1:18, SQUARE_1:22;
then 1 * (1 - sn) = ((p1 `2) / |.p1.|) - sn by A40, XCMPLX_1:87;
then 1 * |.p1.| = p1 `2 by A28, TOPRNS_1:24, XCMPLX_1:87;
then p1 `1 = 0 by A38, XCMPLX_1:6;
hence x1 = x2 by A5, A34, Th82; :: thesis: verum

end;

case A43: ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| >= sn & p2 `1 >= 0 ) ; :: thesis: x1 = x2

0 <= (p1 `1) ^2 by XREAL_1:63;
then ( |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) & 0 + ((p1 `2) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then ((p1 `2) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2) by XREAL_1:72;
then ((p1 `2) ^2) / (|.p1.| ^2) <= 1 by A29, XCMPLX_1:60;
then ((p1 `2) / |.p1.|) ^2 <= 1 by XCMPLX_1:76;
then 1 >= (p1 `2) / |.p1.| by SQUARE_1:51;
then 1 - sn >= ((p1 `2) / |.p1.|) - sn by XREAL_1:9;
then - (1 - sn) <= - (((p1 `2) / |.p1.|) - sn) by XREAL_1:24;
then (- (1 - sn)) / (1 - sn) <= (- (((p1 `2) / |.p1.|) - sn)) / (1 - sn) by A6, XREAL_1:72;
then A44: - 1 <= (- (((p1 `2) / |.p1.|) - sn)) / (1 - sn) by A6, XCMPLX_1:197;
((p1 `2) / |.p1.|) - sn >= 0 by A28, XREAL_1:48;
then ((- (((p1 `2) / |.p1.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A6, A44, SQUARE_1:49;
then 1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 - sn)) ^2) >= 0 by XREAL_1:48;
then A45: 1 - ((- ((((p1 `2) / |.p1.|) - sn) / (1 - sn))) ^2) >= 0 by XCMPLX_1:187;
|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| `1 = |.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2))) by EUCLID:52;
then A46: (|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| `1) ^2 = (|.p1.| ^2) * ((sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2))) ^2)
.= (|.p1.| ^2) * (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)) by A45, SQUARE_1:def 2 ;
A47: |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| `2 = |.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)) by EUCLID:52;
|.|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]|.| ^2 = ((|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| `1) ^2) + ((|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| `2) ^2) by JGRAPH_3:1
.= |.p1.| ^2 by A47, A46 ;
then A48: sqrt (|.|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]|.| ^2) = |.p1.| by SQUARE_1:22;
then A49: |.|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]|.| = |.p1.| by SQUARE_1:22;
0 <= (p2 `1) ^2 by XREAL_1:63;
then ( |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) & 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then A50: ((p2 `2) ^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 `2) ^2) / (|.p2.| ^2) <= 1 by A50, XCMPLX_1:60;
then ((p2 `2) / |.p2.|) ^2 <= 1 by XCMPLX_1:76;
then 1 >= (p2 `2) / |.p2.| by SQUARE_1:51;
then 1 - sn >= ((p2 `2) / |.p2.|) - sn by XREAL_1:9;
then - (1 - sn) <= - (((p2 `2) / |.p2.|) - sn) by XREAL_1:24;
then (- (1 - sn)) / (1 - sn) <= (- (((p2 `2) / |.p2.|) - sn)) / (1 - sn) by A6, XREAL_1:72;
then A51: - 1 <= (- (((p2 `2) / |.p2.|) - sn)) / (1 - sn) by A6, XCMPLX_1:197;
((p2 `2) / |.p2.|) - sn >= 0 by A43, XREAL_1:48;
then ((- (((p2 `2) / |.p2.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A6, A51, SQUARE_1:49;
then 1 - (((- (((p2 `2) / |.p2.|) - sn)) / (1 - sn)) ^2) >= 0 by XREAL_1:48;
then A52: 1 - ((- ((((p2 `2) / |.p2.|) - sn) / (1 - sn))) ^2) >= 0 by XCMPLX_1:187;
set p4 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|;
A53: |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| `2 = |.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)) by EUCLID:52;
|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| `1 = |.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2))) by EUCLID:52;
then A54: (|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| `1) ^2 = (|.p2.| ^2) * ((sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2))) ^2)
.= (|.p2.| ^2) * (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)) by A52, SQUARE_1:def 2 ;
|.|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|.| ^2 = ((|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| `1) ^2) + ((|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| `2) ^2) by JGRAPH_3:1
.= |.p2.| ^2 by A53, A54 ;
then A55: sqrt (|.|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|.| ^2) = |.p2.| by SQUARE_1:22;
then A56: |.|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|.| = |.p2.| by SQUARE_1:22;
A57: (sn -FanMorphE) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| by A1, A2, A43, Th84;
then (((p2 `2) / |.p2.|) - sn) / (1 - sn) = (|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn))) / |.p2.| by A5, A31, A30, A43, A53, TOPRNS_1:24, XCMPLX_1:89;
then (((p2 `2) / |.p2.|) - sn) / (1 - sn) = (((p1 `2) / |.p1.|) - sn) / (1 - sn) by A5, A31, A43, A57, A48, A55, TOPRNS_1:24, XCMPLX_1:89;
then ((((p2 `2) / |.p2.|) - sn) / (1 - sn)) * (1 - sn) = ((p1 `2) / |.p1.|) - sn by A6, XCMPLX_1:87;
then ((p2 `2) / |.p2.|) - sn = ((p1 `2) / |.p1.|) - sn by A6, XCMPLX_1:87;
then ((p2 `2) / |.p2.|) * |.p2.| = p1 `2 by A5, A31, A43, A57, A49, A56, TOPRNS_1:24, XCMPLX_1:87;
then A58: p2 `2 = p1 `2 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 `1 = sqrt ((p1 `1) ^2) by A5, A31, A43, A57, A49, A56, A58, SQUARE_1:22;
then p2 `1 = p1 `1 by A28, SQUARE_1:22;
hence x1 = x2 by A58, A59, EUCLID:53; :: thesis: verum

end;

case A60: ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| < sn & p2 `1 >= 0 ) ; :: thesis: x1 = x2

then ((p2 `2) / |.p2.|) - sn < 0 by XREAL_1:49;
then A61: (((p2 `2) / |.p2.|) - sn) / (1 + sn) < 0 by A1, XREAL_1:141, XREAL_1:148;
set p4 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|;
A62: ( |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| `2 = |.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)) & ((p1 `2) / |.p1.|) - sn >= 0 ) by A28, EUCLID:52, XREAL_1:48;
A63: 1 - sn > 0 by A2, XREAL_1:149;
( (sn -FanMorphE) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| & |.p2.| <> 0 ) by A1, A2, A60, Th84, TOPRNS_1:24;
hence x1 = x2 by A5, A31, A30, A61, A62, A63, XREAL_1:132; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case A64: ( (p1 `2) / |.p1.| < sn & p1 `1 >= 0 & p1 <> 0. (TOP-REAL 2) ) ; :: thesis: x1 = x2

then A65: |.p1.| <> 0 by TOPRNS_1:24;
then A66: |.p1.| ^2 > 0 by SQUARE_1:12;
set q4 = |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]|;
A67: |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| `2 = |.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)) by EUCLID:52;
A68: (sn -FanMorphE) . p1 = |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| by A1, A2, A64, Th84;
A69: |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| `1 = |.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2))) by EUCLID:52;

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

per cases ( p2 `1 <= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| >= sn & p2 `1 >= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| < sn & p2 `1 >= 0 ) ) by JGRAPH_2:3;

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

A71: |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
A72: 1 + sn > 0 by A1, XREAL_1:148;
0 <= (p1 `1) ^2 by XREAL_1:63;
then 0 + ((p1 `2) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2) by XREAL_1:7;
then ((p1 `2) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2) by A71, XREAL_1:72;
then ((p1 `2) ^2) / (|.p1.| ^2) <= 1 by A66, XCMPLX_1:60;
then ((p1 `2) / |.p1.|) ^2 <= 1 by XCMPLX_1:76;
then (- ((p1 `2) / |.p1.|)) ^2 <= 1 ;
then 1 >= - ((p1 `2) / |.p1.|) by SQUARE_1:51;
then 1 + sn >= (- ((p1 `2) / |.p1.|)) + sn by XREAL_1:7;
then A73: (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) <= 1 by A72, XREAL_1:185;
A74: ((p1 `2) / |.p1.|) - sn <= 0 by A64, XREAL_1:47;
then - 1 <= (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) by A72;
then ((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A73, SQUARE_1:49;
then A75: 1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2) >= 0 by XREAL_1:48;
then A76: 1 - ((- ((((p1 `2) / |.p1.|) - sn) / (1 + sn))) ^2) >= 0 by XCMPLX_1:187;
A77: (sn -FanMorphE) . p2 = p2 by A70, Th82;
sqrt (1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2)) >= 0 by A75, SQUARE_1:def 2;
then sqrt (1 - (((- (((p1 `2) / |.p1.|) - sn)) ^2) / ((1 + sn) ^2))) >= 0 by XCMPLX_1:76;
then sqrt (1 - (((((p1 `2) / |.p1.|) - sn) ^2) / ((1 + sn) ^2))) >= 0 ;
then sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)) >= 0 by XCMPLX_1:76;
then p2 `1 = 0 by A5, A68, A70, A77, EUCLID:52;
then sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)) = 0 by A5, A68, A69, A65, A77, XCMPLX_1:6;
then 1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2) = 0 by A76, SQUARE_1:24;
then 1 = sqrt ((- ((((p1 `2) / |.p1.|) - sn) / (1 + sn))) ^2) ;
then 1 = - ((((p1 `2) / |.p1.|) - sn) / (1 + sn)) by A72, A74, SQUARE_1:22;
then 1 = (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) by XCMPLX_1:187;
then 1 * (1 + sn) = - (((p1 `2) / |.p1.|) - sn) by A72, XCMPLX_1:87;
then (1 + sn) - sn = - ((p1 `2) / |.p1.|) ;
then 1 = (- (p1 `2)) / |.p1.| by XCMPLX_1:187;
then 1 * |.p1.| = - (p1 `2) by A64, TOPRNS_1:24, XCMPLX_1:87;
then ((p1 `2) ^2) - ((p1 `2) ^2) = (p1 `1) ^2 by A71, XCMPLX_1:26;
then p1 `1 = 0 by XCMPLX_1:6;
hence x1 = x2 by A5, A77, Th82; :: thesis: verum

end;

case A78: ( p2 <> 0. (TOP-REAL 2) & (p2 `2) / |.p2.| >= sn & p2 `1 >= 0 ) ; :: thesis: x1 = x2

set p4 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|;
A79: ( |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| `2 = |.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)) & |.p1.| <> 0 ) by A64, EUCLID:52, TOPRNS_1:24;
((p1 `2) / |.p1.|) - sn < 0 by A64, XREAL_1:49;
then A80: (((p1 `2) / |.p1.|) - sn) / (1 + sn) < 0 by A1, XREAL_1:141, XREAL_1:148;
A81: 1 - sn > 0 by A2, XREAL_1:149;
( (sn -FanMorphE) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| & ((p2 `2) / |.p2.|) - sn >= 0 ) by A1, A2, A78, Th84, XREAL_1:48;
hence x1 = x2 by A5, A68, A67, A80, A79, A81, XREAL_1:132; :: thesis: verum

end;

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

0 <= (p2 `1) ^2 by XREAL_1:63;
then ( |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) & 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then A83: ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by XREAL_1:72;
A84: 1 + sn > 0 by A1, XREAL_1:148;
0 <= (p1 `1) ^2 by XREAL_1:63;
then ( |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) & 0 + ((p1 `2) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then ((p1 `2) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2) by XREAL_1:72;
then ((p1 `2) ^2) / (|.p1.| ^2) <= 1 by A66, XCMPLX_1:60;
then ((p1 `2) / |.p1.|) ^2 <= 1 by XCMPLX_1:76;
then - 1 <= (p1 `2) / |.p1.| by SQUARE_1:51;
then (- 1) - sn <= ((p1 `2) / |.p1.|) - sn by XREAL_1:9;
then - ((- 1) - sn) >= - (((p1 `2) / |.p1.|) - sn) by XREAL_1:24;
then A85: (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) <= 1 by A84, XREAL_1:185;
((p1 `2) / |.p1.|) - sn <= 0 by A64, XREAL_1:47;
then - 1 <= (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) by A84;
then ((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A85, SQUARE_1:49;
then 1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2) >= 0 by XREAL_1:48;
then A86: 1 - ((- ((((p1 `2) / |.p1.|) - sn) / (1 + sn))) ^2) >= 0 by XCMPLX_1:187;
|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| `1 = |.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2))) by EUCLID:52;
then A87: (|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| `1) ^2 = (|.p1.| ^2) * ((sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2))) ^2)
.= (|.p1.| ^2) * (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)) by A86, SQUARE_1:def 2 ;
A88: |[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| `2 = |.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)) by EUCLID:52;
set p4 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|;
A89: |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| `2 = |.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)) by EUCLID:52;
|.p2.| <> 0 by A82, TOPRNS_1:24;
then |.p2.| ^2 > 0 by SQUARE_1:12;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A83, XCMPLX_1:60;
then ((p2 `2) / |.p2.|) ^2 <= 1 by XCMPLX_1:76;
then - 1 <= (p2 `2) / |.p2.| by SQUARE_1:51;
then (- 1) - sn <= ((p2 `2) / |.p2.|) - sn by XREAL_1:9;
then - ((- 1) - sn) >= - (((p2 `2) / |.p2.|) - sn) by XREAL_1:24;
then A90: (- (((p2 `2) / |.p2.|) - sn)) / (1 + sn) <= 1 by A84, XREAL_1:185;
((p2 `2) / |.p2.|) - sn <= 0 by A82, XREAL_1:47;
then - 1 <= (- (((p2 `2) / |.p2.|) - sn)) / (1 + sn) by A84;
then ((- (((p2 `2) / |.p2.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A90, SQUARE_1:49;
then 1 - (((- (((p2 `2) / |.p2.|) - sn)) / (1 + sn)) ^2) >= 0 by XREAL_1:48;
then A91: 1 - ((- ((((p2 `2) / |.p2.|) - sn) / (1 + sn))) ^2) >= 0 by XCMPLX_1:187;
|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| `1 = |.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))) by EUCLID:52;
then A92: (|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| `1) ^2 = (|.p2.| ^2) * ((sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))) ^2)
.= (|.p2.| ^2) * (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)) by A91, SQUARE_1:def 2 ;
|.|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|.| ^2 = ((|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| `1) ^2) + ((|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| `2) ^2) by JGRAPH_3:1
.= |.p2.| ^2 by A89, A92 ;
then A93: sqrt (|.|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|.| ^2) = |.p2.| by SQUARE_1:22;
then A94: |.|[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|.| = |.p2.| by SQUARE_1:22;
|.|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]|.| ^2 = ((|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| `1) ^2) + ((|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| `2) ^2) by JGRAPH_3:1
.= |.p1.| ^2 by A88, A87 ;
then A95: sqrt (|.|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]|.| ^2) = |.p1.| by SQUARE_1:22;
then A96: |.|[(|.p1.| * (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2)))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]|.| = |.p1.| by SQUARE_1:22;
A97: (sn -FanMorphE) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2)))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| by A1, A2, A82, Th84;
then (((p2 `2) / |.p2.|) - sn) / (1 + sn) = (|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn))) / |.p2.| by A5, A68, A67, A82, A89, TOPRNS_1:24, XCMPLX_1:89;
then (((p2 `2) / |.p2.|) - sn) / (1 + sn) = (((p1 `2) / |.p1.|) - sn) / (1 + sn) by A5, A68, A82, A97, A95, A93, TOPRNS_1:24, XCMPLX_1:89;
then ((((p2 `2) / |.p2.|) - sn) / (1 + sn)) * (1 + sn) = ((p1 `2) / |.p1.|) - sn by A84, XCMPLX_1:87;
then ((p2 `2) / |.p2.|) - sn = ((p1 `2) / |.p1.|) - sn by A84, XCMPLX_1:87;
then ((p2 `2) / |.p2.|) * |.p2.| = p1 `2 by A5, A68, A82, A97, A96, A94, TOPRNS_1:24, XCMPLX_1:87;
then A98: p2 `2 = p1 `2 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 `1 = sqrt ((p1 `1) ^2) by A5, A68, A82, A97, A96, A94, A98, SQUARE_1:22;
then p2 `1 = p1 `1 by A64, SQUARE_1:22;
hence x1 = x2 by A98, A99, EUCLID:53; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

hence sn -FanMorphE is one-to-one by FUNCT_1:def 4; :: thesis: verum