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

proof

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

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;

suppose A7: p1 `2 >= 0 ; :: thesis: x1 = x2

then A8: (cn -FanMorphS) . p1 = p1 by Th113;

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;

suppose p2 `2 >= 0 ; :: thesis: x1 = x2

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

end;

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

then A10: |.p2.| <> 0 by TOPRNS_1:24;
then A11: |.p2.| ^2 > 0 by SQUARE_1:12;
A12: ((p2 `1) / |.p2.|) - cn >= 0 by A9, XREAL_1:48;
A13: |.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 ((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by A13, XREAL_1:72;
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 A14: - 1 <= (- (((p2 `1) / |.p2.|) - cn)) / (1 - cn) by A6, XCMPLX_1:197;
A15: (cn -FanMorphS) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]| by A1, A2, A9, Th115;
then A16: p1 `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))) by A5, A8, EUCLID:52;
((p2 `1) / |.p2.|) - cn >= 0 by A9, XREAL_1:48;
then ((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A6, A14, SQUARE_1:49;
then A17: 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 p1 `2 = 0 by A5, A7, A8, A15, EUCLID:52;
then A18: - (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2))) = - 0 by A16, A10, XCMPLX_1:6;
1 - ((- ((((p2 `1) / |.p2.|) - cn) / (1 - cn))) ^2) >= 0 by A17, XCMPLX_1:187;
then 1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2) = 0 by A18, SQUARE_1:24;
then 1 = (((p2 `1) / |.p2.|) - cn) / (1 - cn) by A6, A12, 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 A9, TOPRNS_1:24, XCMPLX_1:87;
then p2 `2 = 0 by A13, XCMPLX_1:6;
hence x1 = x2 by A5, A8, Th113; :: thesis: verum

end;

suppose A19: ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| < cn & p2 `2 <= 0 ) ; :: thesis: x1 = x2

then A20: (cn -FanMorphS) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]| by A1, A2, Th115;
then A21: p1 `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))) by A5, A8, EUCLID:52;
A22: |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
A23: |.p2.| <> 0 by A19, TOPRNS_1:24;
then A24: |.p2.| ^2 > 0 by SQUARE_1:12;
A25: 1 + cn > 0 by A1, XREAL_1:148;
A26: ((p2 `1) / |.p2.|) - cn <= 0 by A19, XREAL_1:47;
then A27: - 1 <= (- (((p2 `1) / |.p2.|) - cn)) / (1 + cn) by A25;
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 A22, XREAL_1:72;
then ((p2 `1) ^2) / (|.p2.| ^2) <= 1 by A24, 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 A25, XREAL_1:185;
then ((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1 ^2 by A27, SQUARE_1:49;
then A28: 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 p1 `2 = 0 by A5, A7, A8, A20, EUCLID:52;
then A29: - (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))) = - 0 by A21, A23, XCMPLX_1:6;
1 - ((- ((((p2 `1) / |.p2.|) - cn) / (1 + cn))) ^2) >= 0 by A28, XCMPLX_1:187;
then 1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2) = 0 by A29, SQUARE_1:24;
then 1 = (- ((((p2 `1) / |.p2.|) - cn) / (1 + cn))) ^2 ;
then 1 = - ((((p2 `1) / |.p2.|) - cn) / (1 + cn)) by A25, A26, SQUARE_1:18, SQUARE_1:22;
then 1 = (- (((p2 `1) / |.p2.|) - cn)) / (1 + cn) by XCMPLX_1:187;
then 1 * (1 + cn) = - (((p2 `1) / |.p2.|) - cn) by A25, 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 A19, TOPRNS_1:24, XCMPLX_1:87;
then ((p2 `1) ^2) - ((p2 `1) ^2) = (p2 `2) ^2 by A22, XCMPLX_1:26;
then p2 `2 = 0 by XCMPLX_1:6;
hence x1 = x2 by A5, A8, Th113; :: thesis: verum

end;

end;

end;

suppose A30: ( (p1 `1) / |.p1.| >= cn & p1 `2 <= 0 & p1 <> 0. (TOP-REAL 2) ) ; :: thesis: x1 = x2

then |.p1.| <> 0 by TOPRNS_1:24;
then A31: |.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)))))]|;
A32: |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)))))]| `1 = |.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn)) by EUCLID:52;
A33: (cn -FanMorphS) . p1 = |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)))))]| by A1, A2, A30, Th115;

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;

suppose A34: p2 `2 >= 0 ; :: thesis: x1 = x2

then A35: (cn -FanMorphS) . p2 = p2 by Th113;
then A36: p2 `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)))) by A5, A33, EUCLID:52;
A37: ((p1 `1) / |.p1.|) - cn >= 0 by A30, XREAL_1:48;
A38: 1 - cn > 0 by A2, XREAL_1:149;
A39: |.p1.| <> 0 by A30, TOPRNS_1:24;
then A40: |.p1.| ^2 > 0 by SQUARE_1:12;
A41: ((p1 `1) / |.p1.|) - cn >= 0 by A30, XREAL_1:48;
A42: |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
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 A42, XREAL_1:72;
then ((p1 `1) ^2) / (|.p1.| ^2) <= 1 by A40, 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 A38, XREAL_1:72;
then - 1 <= (- (((p1 `1) / |.p1.|) - cn)) / (1 - cn) by A38, XCMPLX_1:197;
then ((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A38, A41, SQUARE_1:49;
then A43: 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, A33, A34, A35, EUCLID:52;
then A44: - (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2))) = - 0 by A36, A39, XCMPLX_1:6;
1 - ((- ((((p1 `1) / |.p1.|) - cn) / (1 - cn))) ^2) >= 0 by A43, XCMPLX_1:187;
then 1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2) = 0 by A44, SQUARE_1:24;
then 1 = (((p1 `1) / |.p1.|) - cn) / (1 - cn) by A38, A37, SQUARE_1:18, SQUARE_1:22;
then 1 * (1 - cn) = ((p1 `1) / |.p1.|) - cn by A38, XCMPLX_1:87;
then 1 * |.p1.| = p1 `1 by A30, TOPRNS_1:24, XCMPLX_1:87;
then p1 `2 = 0 by A42, XCMPLX_1:6;
hence x1 = x2 by A5, A35, Th113; :: thesis: verum

end;

suppose A45: ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| >= cn & p2 `2 <= 0 ) ; :: thesis: 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 A31, 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 A46: - 1 <= (- (((p1 `1) / |.p1.|) - cn)) / (1 - cn) by A6, XCMPLX_1:197;
((p1 `1) / |.p1.|) - cn >= 0 by A30, XREAL_1:48;
then ((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A6, A46, SQUARE_1:49;
then 1 - (((- (((p1 `1) / |.p1.|) - cn)) / (1 - cn)) ^2) >= 0 by XREAL_1:48;
then A47: 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 A48: (|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)))))]| `2) ^2 = (|.p1.| ^2) * ((sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2))) ^2)
.= (|.p1.| ^2) * (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)) by A47, SQUARE_1:def 2 ;
A49: |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)))))]| `1 = |.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn)) by EUCLID: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 A49, A48 ;
then A50: sqrt (|.|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 - cn)) ^2)))))]|.| ^2) = |.p1.| by SQUARE_1:22;
then A51: |.|[(|.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 A52: ((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by XREAL_1:72;
|.p2.| <> 0 by A45, TOPRNS_1:24;
then |.p2.| ^2 > 0 by SQUARE_1:12;
then ((p2 `1) ^2) / (|.p2.| ^2) <= 1 by A52, 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 A53: - 1 <= (- (((p2 `1) / |.p2.|) - cn)) / (1 - cn) by A6, XCMPLX_1:197;
((p2 `1) / |.p2.|) - cn >= 0 by A45, XREAL_1:48;
then ((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A6, A53, SQUARE_1:49;
then 1 - (((- (((p2 `1) / |.p2.|) - cn)) / (1 - cn)) ^2) >= 0 by XREAL_1:48;
then A54: 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)))))]|;
A55: |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]| `1 = |.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn)) by EUCLID: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 A56: (|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]| `2) ^2 = (|.p2.| ^2) * ((sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2))) ^2)
.= (|.p2.| ^2) * (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)) by A54, SQUARE_1:def 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 A55, A56 ;
then A57: sqrt (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]|.| ^2) = |.p2.| by SQUARE_1:22;
then A58: |.|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]|.| = |.p2.| by SQUARE_1:22;
A59: (cn -FanMorphS) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]| by A1, A2, A45, Th115;
then (((p2 `1) / |.p2.|) - cn) / (1 - cn) = (|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 - cn))) / |.p2.| by A5, A33, A32, A45, A55, TOPRNS_1:24, XCMPLX_1:89;
then (((p2 `1) / |.p2.|) - cn) / (1 - cn) = (((p1 `1) / |.p1.|) - cn) / (1 - cn) by A5, A33, A45, A59, A50, A57, 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, A33, A45, A59, A51, A58, TOPRNS_1:24, XCMPLX_1:87;
then A60: p2 `1 = p1 `1 by A45, TOPRNS_1:24, 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 `2)) ^2 = (p1 `2) ^2 by A5, A33, A59, A51, A58, A60;
then - (p2 `2) = sqrt ((- (p1 `2)) ^2) by A45, SQUARE_1:22;
then A61: - (- (p2 `2)) = - (- (p1 `2)) by A30, SQUARE_1:22;
p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
hence x1 = x2 by A60, A61, EUCLID:53; :: thesis: verum

end;

suppose A62: ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| < cn & p2 `2 <= 0 ) ; :: thesis: x1 = x2

then ((p2 `1) / |.p2.|) - cn < 0 by XREAL_1:49;
then A63: (((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)))))]|;
A64: ( |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]| `1 = |.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn)) & ((p1 `1) / |.p1.|) - cn >= 0 ) by A30, EUCLID:52, XREAL_1:48;
A65: 1 - cn > 0 by A2, XREAL_1:149;
( (cn -FanMorphS) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]| & |.p2.| <> 0 ) by A1, A2, A62, Th115, TOPRNS_1:24;
hence x1 = x2 by A5, A33, A32, A63, A64, A65, XREAL_1:132; :: thesis: verum

end;

end;

end;

suppose A66: ( (p1 `1) / |.p1.| < cn & p1 `2 <= 0 & p1 <> 0. (TOP-REAL 2) ) ; :: thesis: x1 = x2

then A67: |.p1.| <> 0 by TOPRNS_1:24;
then A68: |.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)))))]|;
A69: |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)))))]| `1 = |.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn)) by EUCLID:52;
A70: (cn -FanMorphS) . p1 = |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)))))]| by A1, A2, A66, Th115;

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;

suppose A71: p2 `2 >= 0 ; :: thesis: x1 = x2

then A72: (cn -FanMorphS) . p2 = p2 by Th113;
then A73: p2 `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)))) by A5, A70, EUCLID:52;
A74: |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
A75: 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 A74, XREAL_1:72;
then ((p1 `1) ^2) / (|.p1.| ^2) <= 1 by A68, 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 A76: (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn) <= 1 by A75, XREAL_1:185;
A77: ((p1 `1) / |.p1.|) - cn <= 0 by A66, XREAL_1:47;
then - 1 <= (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn) by A75;
then ((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1 ^2 by A76, SQUARE_1:49;
then A78: 1 - (((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2) >= 0 by XREAL_1:48;
then A79: 1 - ((- ((((p1 `1) / |.p1.|) - cn) / (1 + cn))) ^2) >= 0 by XCMPLX_1:187;
sqrt (1 - (((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2)) >= 0 by A78, 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, A70, A71, A72, EUCLID:52;
then - (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2))) = - 0 by A67, A73, XCMPLX_1:6;
then 1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2) = 0 by A79, SQUARE_1:24;
then 1 = (- ((((p1 `1) / |.p1.|) - cn) / (1 + cn))) ^2 ;
then 1 = - ((((p1 `1) / |.p1.|) - cn) / (1 + cn)) by A75, A77, SQUARE_1:18, SQUARE_1:22;
then 1 = (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn) by XCMPLX_1:187;
then 1 * (1 + cn) = - (((p1 `1) / |.p1.|) - cn) by A75, 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 A66, TOPRNS_1:24, XCMPLX_1:87;
then ((p1 `1) ^2) - ((p1 `1) ^2) = (p1 `2) ^2 by A74, XCMPLX_1:26;
then p1 `2 = 0 by XCMPLX_1:6;
hence x1 = x2 by A5, A72, Th113; :: thesis: verum

end;

suppose A80: ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| >= cn & p2 `2 <= 0 ) ; :: thesis: x1 = x2

set p4 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]|;
A81: ( |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]| `1 = |.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn)) & |.p1.| <> 0 ) by A66, EUCLID:52, TOPRNS_1:24;
((p1 `1) / |.p1.|) - cn < 0 by A66, XREAL_1:49;
then A82: (((p1 `1) / |.p1.|) - cn) / (1 + cn) < 0 by A1, XREAL_1:141, XREAL_1:148;
A83: 1 - cn > 0 by A2, XREAL_1:149;
( (cn -FanMorphS) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 - cn)) ^2)))))]| & ((p2 `1) / |.p2.|) - cn >= 0 ) by A1, A2, A80, Th115, XREAL_1:48;
hence x1 = x2 by A5, A70, A69, A82, A81, A83, XREAL_1:132; :: thesis: verum

end;

suppose A84: ( p2 <> 0. (TOP-REAL 2) & (p2 `1) / |.p2.| < cn & p2 `2 <= 0 ) ; :: thesis: 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 A85: ((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by XREAL_1:72;
A86: 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 A68, 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 A87: (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn) <= 1 by A86, XREAL_1:185;
((p1 `1) / |.p1.|) - cn <= 0 by A66, XREAL_1:47;
then - 1 <= (- (((p1 `1) / |.p1.|) - cn)) / (1 + cn) by A86;
then ((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1 ^2 by A87, SQUARE_1:49;
then 1 - (((- (((p1 `1) / |.p1.|) - cn)) / (1 + cn)) ^2) >= 0 by XREAL_1:48;
then A88: 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 A89: (|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)))))]| `2) ^2 = (|.p1.| ^2) * ((sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2))) ^2)
.= (|.p1.| ^2) * (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)) by A88, SQUARE_1:def 2 ;
A90: |[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)))))]| `1 = |.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn)) by EUCLID:52;
set p4 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]|;
A91: |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]| `1 = |.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn)) by EUCLID:52;
|.p2.| <> 0 by A84, TOPRNS_1:24;
then |.p2.| ^2 > 0 by SQUARE_1:12;
then ((p2 `1) ^2) / (|.p2.| ^2) <= 1 by A85, 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 A92: (- (((p2 `1) / |.p2.|) - cn)) / (1 + cn) <= 1 by A86, XREAL_1:185;
((p2 `1) / |.p2.|) - cn <= 0 by A84, XREAL_1:47;
then - 1 <= (- (((p2 `1) / |.p2.|) - cn)) / (1 + cn) by A86;
then ((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1 ^2 by A92, SQUARE_1:49;
then 1 - (((- (((p2 `1) / |.p2.|) - cn)) / (1 + cn)) ^2) >= 0 by XREAL_1:48;
then A93: 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 A94: (|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]| `2) ^2 = (|.p2.| ^2) * ((sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2))) ^2)
.= (|.p2.| ^2) * (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)) by A93, SQUARE_1:def 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 A91, A94 ;
then A95: sqrt (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]|.| ^2) = |.p2.| by SQUARE_1:22;
then A96: |.|[(|.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 A90, A89 ;
then A97: sqrt (|.|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)))))]|.| ^2) = |.p1.| by SQUARE_1:22;
then A98: |.|[(|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1) / |.p1.|) - cn) / (1 + cn)) ^2)))))]|.| = |.p1.| by SQUARE_1:22;
A99: (cn -FanMorphS) . p2 = |[(|.p2.| * ((((p2 `1) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1) / |.p2.|) - cn) / (1 + cn)) ^2)))))]| by A1, A2, A84, Th115;
then (((p2 `1) / |.p2.|) - cn) / (1 + cn) = (|.p1.| * ((((p1 `1) / |.p1.|) - cn) / (1 + cn))) / |.p2.| by A5, A70, A69, A84, A91, TOPRNS_1:24, XCMPLX_1:89;
then (((p2 `1) / |.p2.|) - cn) / (1 + cn) = (((p1 `1) / |.p1.|) - cn) / (1 + cn) by A5, A70, A84, A99, A97, A95, TOPRNS_1:24, XCMPLX_1:89;
then ((((p2 `1) / |.p2.|) - cn) / (1 + cn)) * (1 + cn) = ((p1 `1) / |.p1.|) - cn by A86, XCMPLX_1:87;
then ((p2 `1) / |.p2.|) - cn = ((p1 `1) / |.p1.|) - cn by A86, XCMPLX_1:87;
then ((p2 `1) / |.p2.|) * |.p2.| = p1 `1 by A5, A70, A84, A99, A98, A96, TOPRNS_1:24, XCMPLX_1:87;
then A100: p2 `1 = p1 `1 by A84, TOPRNS_1:24, 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 `2)) ^2 = (p1 `2) ^2 by A5, A70, A99, A98, A96, A100;
then - (p2 `2) = sqrt ((- (p1 `2)) ^2) by A84, SQUARE_1:22;
then A101: - (- (p2 `2)) = - (- (p1 `2)) by A66, SQUARE_1:22;
p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
hence x1 = x2 by A100, A101, EUCLID:53; :: thesis: verum

end;

end;

end;

end;

end;

hence cn -FanMorphS is one-to-one by FUNCT_1:def 4; :: thesis: verum