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

proof

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

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, Th16; :: thesis: verum

end;

case A9: ( 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)))]|;
A10: |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
0 <= (p2 `1) ^2 by XREAL_1:63;
then 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) by XREAL_1:7;
then A11: ((p2 `2) ^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 `2) ^2) / (|.p2.| ^2) <= 1 by A11, 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 A13: - 1 <= (- (((p2 `2) / |.p2.|) - sn)) / (1 - sn) by A6, XCMPLX_1:197;
A14: ((p2 `2) / |.p2.|) - sn >= 0 by A9, XREAL_1:48;
A15: (sn -FanMorphW) . p2 = |[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| by A1, A2, A9, Th18;
((p2 `2) / |.p2.|) - sn >= 0 by A9, XREAL_1:48;
then ((- (((p2 `2) / |.p2.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A6, A13, 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, A14, 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 A12, XCMPLX_1:87;
then p2 `1 = 0 by A10, XCMPLX_1:6;
hence x1 = x2 by A5, A8, Th16; :: thesis: verum

end;

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

then A19: (sn -FanMorphW) . p2 = |[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| by A1, A2, Th18;
set p4 = |[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|;
A20: |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
0 <= (p2 `1) ^2 by XREAL_1:63;
then 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) by XREAL_1:7;
then A21: ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by A20, XREAL_1:72;
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: |.p2.| > 0 by A18, Lm1;
then |.p2.| ^2 > 0 by SQUARE_1:12;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A21, 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, A19, EUCLID:52;
then A27: - (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))) = 0 by A5, A8, A19, A25, 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 A25, XCMPLX_1:87;
then ((p2 `2) ^2) - ((p2 `2) ^2) = (p2 `1) ^2 by A20, XCMPLX_1:26;
then p2 `1 = 0 by XCMPLX_1:6;
hence x1 = x2 by A5, A8, Th16; :: 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 Lm1;
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 -FanMorphW) . p1 = |[(|.p1.| * (- (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2))))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn)))]| by A1, A2, A28, Th18;
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

A34: ((p1 `2) / |.p1.|) - sn >= 0 by A28, XREAL_1:48;
A35: |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
0 <= (p1 `1) ^2 by XREAL_1:63;
then 0 + ((p1 `2) ^2) <= ((p1 `1) ^2) + ((p1 `2) ^2) by XREAL_1:7;
then A36: ((p1 `2) ^2) / (|.p1.| ^2) <= (|.p1.| ^2) / (|.p1.| ^2) by A35, XREAL_1:72;
A37: (sn -FanMorphW) . p2 = p2 by A33, Th16;
A38: ((p1 `2) / |.p1.|) - sn >= 0 by A28, XREAL_1:48;
A39: 1 - sn > 0 by A2, XREAL_1:149;
A40: |.p1.| > 0 by A28, Lm1;
then |.p1.| ^2 > 0 by SQUARE_1:12;
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 A39, XREAL_1:72;
then - 1 <= (- (((p1 `2) / |.p1.|) - sn)) / (1 - sn) by A39, XCMPLX_1:197;
then ((- (((p1 `2) / |.p1.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A39, A34, 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, A37, EUCLID:52;
then A42: - (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 - sn)) ^2))) = 0 by A5, A31, A32, A37, A40, 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 A39, A38, SQUARE_1:18, SQUARE_1:22;
then 1 * (1 - sn) = ((p1 `2) / |.p1.|) - sn by A39, XCMPLX_1:87;
then 1 * |.p1.| = p1 `2 by A40, XCMPLX_1:87;
then p1 `1 = 0 by A35, XCMPLX_1:6;
hence x1 = x2 by A5, A37, Th16; :: 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 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 A48: |.|[(|.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 A49: ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by XREAL_1:72;
A50: |.p2.| > 0 by A43, Lm1;
then |.p2.| ^2 > 0 by SQUARE_1:12;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A49, 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;
set p4 = |[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|;
A52: |[(|.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 `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 A53: 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 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 A53, 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 A52, A54 ;
then 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 A55: |.|[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]|.| = |.p2.| by SQUARE_1:22;
A56: (sn -FanMorphW) . p2 = |[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 - sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 - sn)))]| by A1, A2, A43, Th18;
then (((p2 `2) / |.p2.|) - sn) / (1 - sn) = (|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 - sn))) / |.p2.| by A5, A31, A30, A52, A50, XCMPLX_1:89;
then (((p2 `2) / |.p2.|) - sn) / (1 - sn) = (((p1 `2) / |.p1.|) - sn) / (1 - sn) by A5, A31, A56, A48, A50, A55, 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, A56, A48, A50, A55, XCMPLX_1:87;
then A57: p2 `2 = p1 `2 by A50, XCMPLX_1:87;
( |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) & |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) ) by JGRAPH_3:1;
then (- (p2 `1)) ^2 = (p1 `1) ^2 by A5, A31, A56, A48, A55, A57;
then - (p2 `1) = sqrt ((- (p1 `1)) ^2) by A43, SQUARE_1:22;
then A58: - (- (p2 `1)) = - (- (p1 `1)) by A28, SQUARE_1:22;
p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
hence x1 = x2 by A57, A58, EUCLID:53; :: thesis: verum

end;

case A59: ( 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 A60: (((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)))]|;
A61: ( |[(|.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;
A62: 1 - sn > 0 by A2, XREAL_1:149;
(sn -FanMorphW) . p2 = |[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| by A1, A2, A59, Th18;
hence x1 = x2 by A5, A31, A30, A59, A60, A61, A62, Lm1, XREAL_1:132; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

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

then A64: |.p1.| > 0 by Lm1;
then A65: |.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)))]|;
A66: |[(|.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;
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 -FanMorphW) . p1 = |[(|.p1.| * (- (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2))))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]| by A1, A2, A63, Th18;

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;

suppose A69: p2 `1 >= 0 ; :: thesis: x1 = x2

A70: |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
A71: 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 A70, XREAL_1:72;
then ((p1 `2) ^2) / (|.p1.| ^2) <= 1 by A65, 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 A72: (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) <= 1 by A71, XREAL_1:185;
A73: ((p1 `2) / |.p1.|) - sn <= 0 by A63, XREAL_1:47;
then - 1 <= (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) by A71;
then ((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A72, SQUARE_1:49;
then A74: 1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2) >= 0 by XREAL_1:48;
then A75: 1 - ((- ((((p1 `2) / |.p1.|) - sn) / (1 + sn))) ^2) >= 0 by XCMPLX_1:187;
A76: (sn -FanMorphW) . p2 = p2 by A69, Th16;
sqrt (1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2)) >= 0 by A74, 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, A69, A76, EUCLID:52;
then - (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2))) = 0 by A5, A68, A66, A64, A76, XCMPLX_1:6;
then 1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2) = 0 by A75, SQUARE_1:24;
then 1 = sqrt ((- ((((p1 `2) / |.p1.|) - sn) / (1 + sn))) ^2) ;
then 1 = - ((((p1 `2) / |.p1.|) - sn) / (1 + sn)) by A71, A73, SQUARE_1:22;
then 1 = (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) by XCMPLX_1:187;
then 1 * (1 + sn) = - (((p1 `2) / |.p1.|) - sn) by A71, 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, XCMPLX_1:87;
then ((p1 `2) ^2) - ((p1 `2) ^2) = (p1 `1) ^2 by A70, XCMPLX_1:26;
then p1 `1 = 0 by XCMPLX_1:6;
hence x1 = x2 by A5, A76, Th16; :: thesis: verum

end;

suppose A77: ( 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)))]|;
A78: ( |[(|.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)) & 1 - sn > 0 ) by A2, EUCLID:52, XREAL_1:149;
((p1 `2) / |.p1.|) - sn < 0 by A63, XREAL_1:49;
then A79: (((p1 `2) / |.p1.|) - sn) / (1 + sn) < 0 by A1, XREAL_1:141, XREAL_1:148;
( (sn -FanMorphW) . 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, A77, Th18, XREAL_1:48;
hence x1 = x2 by A5, A63, A68, A67, A79, A78, Lm1, XREAL_1:132; :: thesis: verum

end;

suppose A80: ( 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 A81: ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by XREAL_1:72;
A82: 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 A65, 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 A83: (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) <= 1 by A82, XREAL_1:185;
((p1 `2) / |.p1.|) - sn <= 0 by A63, XREAL_1:47;
then - 1 <= (- (((p1 `2) / |.p1.|) - sn)) / (1 + sn) by A82;
then ((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A83, SQUARE_1:49;
then 1 - (((- (((p1 `2) / |.p1.|) - sn)) / (1 + sn)) ^2) >= 0 by XREAL_1:48;
then A84: 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 A85: (|[(|.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 A84, SQUARE_1:def 2 ;
A86: |[(|.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)))]|;
A87: |[(|.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;
|.|[(|.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 A86, A85 ;
then 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 A88: |.|[(|.p1.| * (- (sqrt (1 - (((((p1 `2) / |.p1.|) - sn) / (1 + sn)) ^2))))),(|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn)))]|.| = |.p1.| by SQUARE_1:22;
((p2 `2) / |.p2.|) - sn <= 0 by A80, XREAL_1:47;
then A89: - 1 <= (- (((p2 `2) / |.p2.|) - sn)) / (1 + sn) by A82;
A90: |.p2.| > 0 by A80, Lm1;
then |.p2.| ^2 > 0 by SQUARE_1:12;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A81, 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 (- (((p2 `2) / |.p2.|) - sn)) / (1 + sn) <= 1 by A82, XREAL_1:185;
then ((- (((p2 `2) / |.p2.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A89, 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 A87, A92 ;
then 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 A93: |.|[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]|.| = |.p2.| by SQUARE_1:22;
A94: (sn -FanMorphW) . p2 = |[(|.p2.| * (- (sqrt (1 - (((((p2 `2) / |.p2.|) - sn) / (1 + sn)) ^2))))),(|.p2.| * ((((p2 `2) / |.p2.|) - sn) / (1 + sn)))]| by A1, A2, A80, Th18;
then (((p2 `2) / |.p2.|) - sn) / (1 + sn) = (|.p1.| * ((((p1 `2) / |.p1.|) - sn) / (1 + sn))) / |.p2.| by A5, A68, A67, A87, A90, XCMPLX_1:89;
then (((p2 `2) / |.p2.|) - sn) / (1 + sn) = (((p1 `2) / |.p1.|) - sn) / (1 + sn) by A5, A68, A94, A88, A90, A93, XCMPLX_1:89;
then ((((p2 `2) / |.p2.|) - sn) / (1 + sn)) * (1 + sn) = ((p1 `2) / |.p1.|) - sn by A82, XCMPLX_1:87;
then ((p2 `2) / |.p2.|) - sn = ((p1 `2) / |.p1.|) - sn by A82, XCMPLX_1:87;
then ((p2 `2) / |.p2.|) * |.p2.| = p1 `2 by A5, A68, A94, A88, A90, A93, XCMPLX_1:87;
then A95: p2 `2 = p1 `2 by A90, XCMPLX_1:87;
( |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) & |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) ) by JGRAPH_3:1;
then (- (p2 `1)) ^2 = (p1 `1) ^2 by A5, A68, A94, A88, A93, A95;
then - (p2 `1) = sqrt ((- (p1 `1)) ^2) by A80, SQUARE_1:22;
then A96: - (- (p2 `1)) = - (- (p1 `1)) by A63, SQUARE_1:22;
p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
hence x1 = x2 by A95, A96, EUCLID:53; :: thesis: verum

end;

end;

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

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