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 set 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 set ; :: 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:151;

now

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

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

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

now

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

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

hence x1 = x2 by A5, A8, Th89; :: 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:50;
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:10;
A12: |.p2.| <> 0 by A9, TOPRNS_1:25;
then A13: |.p2.| ^2 > 0 by SQUARE_1:74;
0 <= (p2 `1 ) ^2 by XREAL_1:65;
then 0 + ((p2 `2 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by XREAL_1:9;
then ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 ) by A11, XREAL_1:74;
then ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= 1 by A13, XCMPLX_1:60;
then ((p2 `2 ) / |.p2.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (p2 `2 ) / |.p2.| by SQUARE_1:121;
then 1 - sn >= ((p2 `2 ) / |.p2.|) - sn by XREAL_1:11;
then - (1 - sn) <= - (((p2 `2 ) / |.p2.|) - sn) by XREAL_1:26;
then (- (1 - sn)) / (1 - sn) <= (- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn) by A6, XREAL_1:74;
then A14: - 1 <= (- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn) by A6, XCMPLX_1:198;
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, Th91;
((p2 `2 ) / |.p2.|) - sn >= 0 by A9, XREAL_1:50;
then ((- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A6, A14, SQUARE_1:119;
then A16: 1 - (((- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn)) ^2 ) >= 0 by XREAL_1:50;
then sqrt (1 - (((- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn)) ^2 )) >= 0 by SQUARE_1:def 4;
then sqrt (1 - (((- (((p2 `2 ) / |.p2.|) - sn)) ^2 ) / ((1 - sn) ^2 ))) >= 0 by XCMPLX_1:77;
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:77;
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:56;
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:188;
then 1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)) ^2 ) = 0 by A17, SQUARE_1:92;
then 1 = (((p2 `2 ) / |.p2.|) - sn) / (1 - sn) by A6, A10, SQUARE_1:83, SQUARE_1:89;
then 1 * (1 - sn) = ((p2 `2 ) / |.p2.|) - sn by A6, XCMPLX_1:88;
then 1 * |.p2.| = p2 `2 by A9, TOPRNS_1:25, XCMPLX_1:88;
then p2 `1 = 0 by A11, XCMPLX_1:6;
hence x1 = x2 by A5, A8, Th89; :: 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:25;
then A20: |.p2.| ^2 > 0 by SQUARE_1:74;
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:10;
A22: 1 + sn > 0 by A1, XREAL_1:150;
A23: ((p2 `2 ) / |.p2.|) - sn <= 0 by A18, XREAL_1:49;
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, Th91;
0 <= (p2 `1 ) ^2 by XREAL_1:65;
then 0 + ((p2 `2 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by XREAL_1:9;
then ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 ) by A21, XREAL_1:74;
then ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= 1 by A20, XCMPLX_1:60;
then ((p2 `2 ) / |.p2.|) ^2 <= 1 by XCMPLX_1:77;
then (- ((p2 `2 ) / |.p2.|)) ^2 <= 1 ;
then 1 >= - ((p2 `2 ) / |.p2.|) by SQUARE_1:121;
then 1 + sn >= (- ((p2 `2 ) / |.p2.|)) + sn by XREAL_1:9;
then (- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn) <= 1 by A22, XREAL_1:187;
then ((- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A24, SQUARE_1:119;
then A26: 1 - (((- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)) ^2 ) >= 0 by XREAL_1:50;
then sqrt (1 - (((- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)) ^2 )) >= 0 by SQUARE_1:def 4;
then sqrt (1 - (((- (((p2 `2 ) / |.p2.|) - sn)) ^2 ) / ((1 + sn) ^2 ))) >= 0 by XCMPLX_1:77;
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:77;
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:56;
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:188;
then 1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 ) = 0 by A27, SQUARE_1:92;
then 1 = sqrt ((- ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn))) ^2 ) by SQUARE_1:83;
then 1 = - ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) by A22, A23, SQUARE_1:89;
then 1 = (- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn) by XCMPLX_1:188;
then 1 * (1 + sn) = - (((p2 `2 ) / |.p2.|) - sn) by A22, XCMPLX_1:88;
then (1 + sn) - sn = - ((p2 `2 ) / |.p2.|) ;
then 1 = (- (p2 `2 )) / |.p2.| by XCMPLX_1:188;
then 1 * |.p2.| = - (p2 `2 ) by A18, TOPRNS_1:25, XCMPLX_1:88;
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, Th89; :: 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:25;
then A29: |.p1.| ^2 > 0 by SQUARE_1:74;
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:56;
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, Th91;
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:56;

now

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

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

then A34: (sn -FanMorphE ) . p2 = p2 by Th89;
A35: |.p1.| <> 0 by A28, TOPRNS_1:25;
then A36: |.p1.| ^2 > 0 by SQUARE_1:74;
A37: ((p1 `2 ) / |.p1.|) - sn >= 0 by A28, XREAL_1:50;
A38: |.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by JGRAPH_3:10;
A39: ((p1 `2 ) / |.p1.|) - sn >= 0 by A28, XREAL_1:50;
A40: 1 - sn > 0 by A2, XREAL_1:151;
0 <= (p1 `1 ) ^2 by XREAL_1:65;
then 0 + ((p1 `2 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by XREAL_1:9;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 ) by A38, XREAL_1:74;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= 1 by A36, XCMPLX_1:60;
then ((p1 `2 ) / |.p1.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (p1 `2 ) / |.p1.| by SQUARE_1:121;
then 1 - sn >= ((p1 `2 ) / |.p1.|) - sn by XREAL_1:11;
then - (1 - sn) <= - (((p1 `2 ) / |.p1.|) - sn) by XREAL_1:26;
then (- (1 - sn)) / (1 - sn) <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn) by A40, XREAL_1:74;
then - 1 <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn) by A40, XCMPLX_1:198;
then ((- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A40, A37, SQUARE_1:119;
then A41: 1 - (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn)) ^2 ) >= 0 by XREAL_1:50;
then sqrt (1 - (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn)) ^2 )) >= 0 by SQUARE_1:def 4;
then sqrt (1 - (((- (((p1 `2 ) / |.p1.|) - sn)) ^2 ) / ((1 - sn) ^2 ))) >= 0 by XCMPLX_1:77;
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:77;
then p2 `1 = 0 by A5, A31, A33, A34, EUCLID:56;
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:188;
then 1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 - sn)) ^2 ) = 0 by A42, SQUARE_1:92;
then 1 = (((p1 `2 ) / |.p1.|) - sn) / (1 - sn) by A40, A39, SQUARE_1:83, SQUARE_1:89;
then 1 * (1 - sn) = ((p1 `2 ) / |.p1.|) - sn by A40, XCMPLX_1:88;
then 1 * |.p1.| = p1 `2 by A28, TOPRNS_1:25, XCMPLX_1:88;
then p1 `1 = 0 by A38, XCMPLX_1:6;
hence x1 = x2 by A5, A34, Th89; :: 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:65;
then ( |.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) & 0 + ((p1 `2 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) ) by JGRAPH_3:10, XREAL_1:9;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 ) by XREAL_1:74;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= 1 by A29, XCMPLX_1:60;
then ((p1 `2 ) / |.p1.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (p1 `2 ) / |.p1.| by SQUARE_1:121;
then 1 - sn >= ((p1 `2 ) / |.p1.|) - sn by XREAL_1:11;
then - (1 - sn) <= - (((p1 `2 ) / |.p1.|) - sn) by XREAL_1:26;
then (- (1 - sn)) / (1 - sn) <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn) by A6, XREAL_1:74;
then A44: - 1 <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn) by A6, XCMPLX_1:198;
((p1 `2 ) / |.p1.|) - sn >= 0 by A28, XREAL_1:50;
then ((- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A6, A44, SQUARE_1:119;
then 1 - (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 - sn)) ^2 ) >= 0 by XREAL_1:50;
then A45: 1 - ((- ((((p1 `2 ) / |.p1.|) - sn) / (1 - sn))) ^2 ) >= 0 by XCMPLX_1:188;
|[(|.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:56;
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 4 ;
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:56;
|.|[(|.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:10
.= |.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:89;
then A49: |.|[(|.p1.| * (sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 - sn)) ^2 )))),(|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 - sn)))]|.| = |.p1.| by SQUARE_1:89;
0 <= (p2 `1 ) ^2 by XREAL_1:65;
then ( |.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) & 0 + ((p2 `2 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) ) by JGRAPH_3:10, XREAL_1:9;
then A50: ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 ) by XREAL_1:74;
|.p2.| <> 0 by A43, TOPRNS_1:25;
then |.p2.| ^2 > 0 by SQUARE_1:74;
then ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= 1 by A50, XCMPLX_1:60;
then ((p2 `2 ) / |.p2.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (p2 `2 ) / |.p2.| by SQUARE_1:121;
then 1 - sn >= ((p2 `2 ) / |.p2.|) - sn by XREAL_1:11;
then - (1 - sn) <= - (((p2 `2 ) / |.p2.|) - sn) by XREAL_1:26;
then (- (1 - sn)) / (1 - sn) <= (- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn) by A6, XREAL_1:74;
then A51: - 1 <= (- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn) by A6, XCMPLX_1:198;
((p2 `2 ) / |.p2.|) - sn >= 0 by A43, XREAL_1:50;
then ((- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A6, A51, SQUARE_1:119;
then 1 - (((- (((p2 `2 ) / |.p2.|) - sn)) / (1 - sn)) ^2 ) >= 0 by XREAL_1:50;
then A52: 1 - ((- ((((p2 `2 ) / |.p2.|) - sn) / (1 - sn))) ^2 ) >= 0 by XCMPLX_1:188;
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:56;
|[(|.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:56;
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 4 ;
|.|[(|.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:10
.= |.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:89;
then A56: |.|[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)))]|.| = |.p2.| by SQUARE_1:89;
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, Th91;
then (((p2 `2 ) / |.p2.|) - sn) / (1 - sn) = (|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 - sn))) / |.p2.| by A5, A31, A30, A43, A53, TOPRNS_1:25, XCMPLX_1:90;
then (((p2 `2 ) / |.p2.|) - sn) / (1 - sn) = (((p1 `2 ) / |.p1.|) - sn) / (1 - sn) by A5, A31, A43, A57, A48, A55, TOPRNS_1:25, XCMPLX_1:90;
then ((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)) * (1 - sn) = ((p1 `2 ) / |.p1.|) - sn by A6, XCMPLX_1:88;
then ((p2 `2 ) / |.p2.|) - sn = ((p1 `2 ) / |.p1.|) - sn by A6, XCMPLX_1:88;
then ((p2 `2 ) / |.p2.|) * |.p2.| = p1 `2 by A5, A31, A43, A57, A49, A56, TOPRNS_1:25, XCMPLX_1:88;
then A58: p2 `2 = p1 `2 by A43, TOPRNS_1:25, XCMPLX_1:88;
A59: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( |.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) & |.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) ) by JGRAPH_3:10;
then p2 `1 = sqrt ((p1 `1 ) ^2 ) by A5, A31, A43, A57, A49, A56, A58, SQUARE_1:89;
then p2 `1 = p1 `1 by A28, SQUARE_1:89;
hence x1 = x2 by A58, A59, EUCLID:57; :: 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:51;
then A61: (((p2 `2 ) / |.p2.|) - sn) / (1 + sn) < 0 by A1, XREAL_1:143, XREAL_1:150;
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:56, XREAL_1:50;
A63: 1 - sn > 0 by A2, XREAL_1:151;
( (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, Th91, TOPRNS_1:25;
hence x1 = x2 by A5, A31, A30, A61, A62, A63, XREAL_1:134; :: 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:25;
then A66: |.p1.| ^2 > 0 by SQUARE_1:74;
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:56;
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, Th91;
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:56;

now

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

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

A71: |.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by JGRAPH_3:10;
A72: 1 + sn > 0 by A1, XREAL_1:150;
0 <= (p1 `1 ) ^2 by XREAL_1:65;
then 0 + ((p1 `2 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by XREAL_1:9;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 ) by A71, XREAL_1:74;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= 1 by A66, XCMPLX_1:60;
then ((p1 `2 ) / |.p1.|) ^2 <= 1 by XCMPLX_1:77;
then (- ((p1 `2 ) / |.p1.|)) ^2 <= 1 ;
then 1 >= - ((p1 `2 ) / |.p1.|) by SQUARE_1:121;
then 1 + sn >= (- ((p1 `2 ) / |.p1.|)) + sn by XREAL_1:9;
then A73: (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn) <= 1 by A72, XREAL_1:187;
A74: ((p1 `2 ) / |.p1.|) - sn <= 0 by A64, XREAL_1:49;
then - 1 <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn) by A72;
then ((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A73, SQUARE_1:119;
then A75: 1 - (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 ) >= 0 by XREAL_1:50;
then A76: 1 - ((- ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn))) ^2 ) >= 0 by XCMPLX_1:188;
A77: (sn -FanMorphE ) . p2 = p2 by A70, Th89;
sqrt (1 - (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 )) >= 0 by A75, SQUARE_1:def 4;
then sqrt (1 - (((- (((p1 `2 ) / |.p1.|) - sn)) ^2 ) / ((1 + sn) ^2 ))) >= 0 by XCMPLX_1:77;
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:77;
then p2 `1 = 0 by A5, A68, A70, A77, EUCLID:56;
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:92;
then 1 = sqrt ((- ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn))) ^2 ) by SQUARE_1:83;
then 1 = - ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) by A72, A74, SQUARE_1:89;
then 1 = (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn) by XCMPLX_1:188;
then 1 * (1 + sn) = - (((p1 `2 ) / |.p1.|) - sn) by A72, XCMPLX_1:88;
then (1 + sn) - sn = - ((p1 `2 ) / |.p1.|) ;
then 1 = (- (p1 `2 )) / |.p1.| by XCMPLX_1:188;
then 1 * |.p1.| = - (p1 `2 ) by A64, TOPRNS_1:25, XCMPLX_1:88;
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, Th89; :: 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:56, TOPRNS_1:25;
((p1 `2 ) / |.p1.|) - sn < 0 by A64, XREAL_1:51;
then A80: (((p1 `2 ) / |.p1.|) - sn) / (1 + sn) < 0 by A1, XREAL_1:143, XREAL_1:150;
A81: 1 - sn > 0 by A2, XREAL_1:151;
( (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, Th91, XREAL_1:50;
hence x1 = x2 by A5, A68, A67, A80, A79, A81, XREAL_1:134; :: 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:65;
then ( |.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) & 0 + ((p2 `2 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) ) by JGRAPH_3:10, XREAL_1:9;
then A83: ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 ) by XREAL_1:74;
A84: 1 + sn > 0 by A1, XREAL_1:150;
0 <= (p1 `1 ) ^2 by XREAL_1:65;
then ( |.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) & 0 + ((p1 `2 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) ) by JGRAPH_3:10, XREAL_1:9;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 ) by XREAL_1:74;
then ((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= 1 by A66, XCMPLX_1:60;
then ((p1 `2 ) / |.p1.|) ^2 <= 1 by XCMPLX_1:77;
then - 1 <= (p1 `2 ) / |.p1.| by SQUARE_1:121;
then (- 1) - sn <= ((p1 `2 ) / |.p1.|) - sn by XREAL_1:11;
then - ((- 1) - sn) >= - (((p1 `2 ) / |.p1.|) - sn) by XREAL_1:26;
then A85: (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn) <= 1 by A84, XREAL_1:187;
((p1 `2 ) / |.p1.|) - sn <= 0 by A64, XREAL_1:49;
then - 1 <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn) by A84;
then ((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A85, SQUARE_1:119;
then 1 - (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 ) >= 0 by XREAL_1:50;
then A86: 1 - ((- ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn))) ^2 ) >= 0 by XCMPLX_1:188;
|[(|.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:56;
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 4 ;
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:56;
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:56;
|.p2.| <> 0 by A82, TOPRNS_1:25;
then |.p2.| ^2 > 0 by SQUARE_1:74;
then ((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= 1 by A83, XCMPLX_1:60;
then ((p2 `2 ) / |.p2.|) ^2 <= 1 by XCMPLX_1:77;
then - 1 <= (p2 `2 ) / |.p2.| by SQUARE_1:121;
then (- 1) - sn <= ((p2 `2 ) / |.p2.|) - sn by XREAL_1:11;
then - ((- 1) - sn) >= - (((p2 `2 ) / |.p2.|) - sn) by XREAL_1:26;
then A90: (- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn) <= 1 by A84, XREAL_1:187;
((p2 `2 ) / |.p2.|) - sn <= 0 by A82, XREAL_1:49;
then - 1 <= (- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn) by A84;
then ((- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A90, SQUARE_1:119;
then 1 - (((- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)) ^2 ) >= 0 by XREAL_1:50;
then A91: 1 - ((- ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn))) ^2 ) >= 0 by XCMPLX_1:188;
|[(|.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:56;
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 4 ;
|.|[(|.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:10
.= |.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:89;
then A94: |.|[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)))]|.| = |.p2.| by SQUARE_1:89;
|.|[(|.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:10
.= |.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:89;
then A96: |.|[(|.p1.| * (sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) ^2 )))),(|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)))]|.| = |.p1.| by SQUARE_1:89;
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, Th91;
then (((p2 `2 ) / |.p2.|) - sn) / (1 + sn) = (|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn))) / |.p2.| by A5, A68, A67, A82, A89, TOPRNS_1:25, XCMPLX_1:90;
then (((p2 `2 ) / |.p2.|) - sn) / (1 + sn) = (((p1 `2 ) / |.p1.|) - sn) / (1 + sn) by A5, A68, A82, A97, A95, A93, TOPRNS_1:25, XCMPLX_1:90;
then ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) * (1 + sn) = ((p1 `2 ) / |.p1.|) - sn by A84, XCMPLX_1:88;
then ((p2 `2 ) / |.p2.|) - sn = ((p1 `2 ) / |.p1.|) - sn by A84, XCMPLX_1:88;
then ((p2 `2 ) / |.p2.|) * |.p2.| = p1 `2 by A5, A68, A82, A97, A96, A94, TOPRNS_1:25, XCMPLX_1:88;
then A98: p2 `2 = p1 `2 by A82, TOPRNS_1:25, XCMPLX_1:88;
A99: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( |.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) & |.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) ) by JGRAPH_3:10;
then p2 `1 = sqrt ((p1 `1 ) ^2 ) by A5, A68, A82, A97, A96, A94, A98, SQUARE_1:89;
then p2 `1 = p1 `1 by A64, SQUARE_1:89;
hence x1 = x2 by A98, A99, EUCLID:57; :: 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 8; :: thesis: verum