let cn be Real; :: thesis: for p being Point of (TOP-REAL 2) holds |.((cn -FanMorphS ) . p).| = |.p.|
let p be Point of (TOP-REAL 2); :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|
set f = cn -FanMorphS ;
set z = (cn -FanMorphS ) . p;
set q = p;
reconsider qz = (cn -FanMorphS ) . p as Point of (TOP-REAL 2) ;

per cases ( ( (p `1 ) / |.p.| >= cn & p `2 < 0 ) or ( (p `1 ) / |.p.| < cn & p `2 < 0 ) or p `2 >= 0 ) ;

suppose A1: ( (p `1 ) / |.p.| >= cn & p `2 < 0 ) ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

then (cn -FanMorphS ) . p = |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 - cn))),(|.p.| * (- (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 - cn)) ^2 )))))]| by Th120;
then A2: ( qz `2 = |.p.| * (- (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 - cn)) ^2 )))) & qz `1 = |.p.| * ((((p `1 ) / |.p.|) - cn) / (1 - cn)) ) by EUCLID:56;
|.p.| <> 0 by A1, JGRAPH_2:11, TOPRNS_1:25;
then A3: |.p.| ^2 > 0 by SQUARE_1:74;
A4: ((p `1 ) / |.p.|) - cn >= 0 by A1, XREAL_1:50;
A5: |.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by JGRAPH_3:10;
0 <= (p `2 ) ^2 by XREAL_1:65;
then 0 + ((p `1 ) ^2 ) <= ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by XREAL_1:9;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) <= (|.p.| ^2 ) / (|.p.| ^2 ) by A5, XREAL_1:74;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) <= 1 by A3, XCMPLX_1:60;
then ((p `1 ) / |.p.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (p `1 ) / |.p.| by SQUARE_1:121;
then A6: 1 - cn >= ((p `1 ) / |.p.|) - cn by XREAL_1:11;

per cases ( 1 - cn = 0 or 1 - cn <> 0 ) ;

suppose A7: 1 - cn = 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

A8: (((p `1 ) / |.p.|) - cn) / (1 - cn) = (((p `1 ) / |.p.|) - cn) * ((1 - cn) " ) by XCMPLX_0:def 9
.= (((p `1 ) / |.p.|) - cn) * 0 by A7
.= 0 ;
then 1 - (((((p `1 ) / |.p.|) - cn) / (1 - cn)) ^2 ) = 1 ;
then (cn -FanMorphS ) . p = |[(|.p.| * 0 ),(|.p.| * (- 1))]| by A1, A8, Th120, SQUARE_1:83
.= |[0 ,(- |.p.|)]| ;
then ( ((cn -FanMorphS ) . p) `2 = - |.p.| & ((cn -FanMorphS ) . p) `1 = 0 ) by EUCLID:56;
then |.((cn -FanMorphS ) . p).| = sqrt (((- |.p.|) ^2 ) + (0 ^2 )) by JGRAPH_3:10
.= sqrt (|.p.| ^2 )
.= |.p.| by SQUARE_1:89 ;
hence |.((cn -FanMorphS ) . p).| = |.p.| ; :: thesis: verum

end;

suppose A9: 1 - cn <> 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

per cases ( 1 - cn > 0 or 1 - cn < 0 ) by A9;

suppose A10: 1 - cn > 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

then A11: - (1 - cn) <= - 0 ;
- (1 - cn) <= - (((p `1 ) / |.p.|) - cn) by A6, XREAL_1:26;
then (- (1 - cn)) / (1 - cn) <= (- (((p `1 ) / |.p.|) - cn)) / (1 - cn) by A10, XREAL_1:74;
then A12: - 1 <= (- (((p `1 ) / |.p.|) - cn)) / (1 - cn) by A10, XCMPLX_1:198;
- (- (1 - cn)) >= - (((p `1 ) / |.p.|) - cn) by A4, A11, XREAL_1:26;
then (- (((p `1 ) / |.p.|) - cn)) / (1 - cn) <= 1 by A10, XREAL_1:187;
then ((- (((p `1 ) / |.p.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A12, SQUARE_1:119;
then 1 - (((- (((p `1 ) / |.p.|) - cn)) / (1 - cn)) ^2 ) >= 0 by XREAL_1:50;
then A13: 1 - ((- ((((p `1 ) / |.p.|) - cn) / (1 - cn))) ^2 ) >= 0 by XCMPLX_1:188;
A14: (qz `2 ) ^2 = (|.p.| ^2 ) * ((sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 - cn)) ^2 ))) ^2 ) by A2
.= (|.p.| ^2 ) * (1 - (((((p `1 ) / |.p.|) - cn) / (1 - cn)) ^2 )) by A13, SQUARE_1:def 4 ;
|.qz.| ^2 = ((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) by JGRAPH_3:10
.= |.p.| ^2 by A2, A14 ;
then sqrt (|.qz.| ^2 ) = |.p.| by SQUARE_1:89;
hence |.((cn -FanMorphS ) . p).| = |.p.| by SQUARE_1:89; :: thesis: verum

end;

suppose A15: 1 - cn < 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

A16: ((p `1 ) / |.p.|) - cn >= 0 by A1, XREAL_1:50;
0 + ((p `1 ) ^2 ) < ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by A1, SQUARE_1:74, XREAL_1:10;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) < (|.p.| ^2 ) / (|.p.| ^2 ) by A3, A5, XREAL_1:76;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) < 1 by A3, XCMPLX_1:60;
then ((p `1 ) / |.p.|) ^2 < 1 by XCMPLX_1:77;
then 1 > (p `1 ) / |.p.| by SQUARE_1:122;
hence |.((cn -FanMorphS ) . p).| = |.p.| by A15, A16, XREAL_1:11; :: thesis: verum

end;

end;

end;

end;

end;

suppose A17: ( (p `1 ) / |.p.| < cn & p `2 < 0 ) ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

then A18: (cn -FanMorphS ) . p = |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))),(|.p.| * (- (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 )))))]| by Th121;
then A19: ( qz `2 = |.p.| * (- (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 )))) & qz `1 = |.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn)) ) by EUCLID:56;
|.p.| <> 0 by A17, JGRAPH_2:11, TOPRNS_1:25;
then A20: |.p.| ^2 > 0 by SQUARE_1:74;
A21: ((p `1 ) / |.p.|) - cn < 0 by A17, XREAL_1:51;
A22: |.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by JGRAPH_3:10;
0 <= (p `2 ) ^2 by XREAL_1:65;
then 0 + ((p `1 ) ^2 ) <= ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by XREAL_1:9;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) <= (|.p.| ^2 ) / (|.p.| ^2 ) by A22, XREAL_1:74;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) <= 1 by A20, XCMPLX_1:60;
then ((p `1 ) / |.p.|) ^2 <= 1 by XCMPLX_1:77;
then - 1 <= (p `1 ) / |.p.| by SQUARE_1:121;
then A23: (- 1) - cn <= ((p `1 ) / |.p.|) - cn by XREAL_1:11;

per cases ( 1 + cn = 0 or 1 + cn <> 0 ) ;

suppose A24: 1 + cn = 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

(((p `1 ) / |.p.|) - cn) / (1 + cn) = (((p `1 ) / |.p.|) - cn) * ((1 + cn) " ) by XCMPLX_0:def 9
.= (((p `1 ) / |.p.|) - cn) * 0 by A24
.= 0 ;
then ( ((cn -FanMorphS ) . p) `2 = - |.p.| & ((cn -FanMorphS ) . p) `1 = 0 ) by A18, EUCLID:56, SQUARE_1:83;
then |.((cn -FanMorphS ) . p).| = sqrt (((- |.p.|) ^2 ) + (0 ^2 )) by JGRAPH_3:10
.= sqrt (|.p.| ^2 )
.= |.p.| by SQUARE_1:89 ;
hence |.((cn -FanMorphS ) . p).| = |.p.| ; :: thesis: verum

end;

suppose A25: 1 + cn <> 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

per cases ( 1 + cn > 0 or 1 + cn < 0 ) by A25;

suppose A26: 1 + cn > 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

then (- (1 + cn)) / (1 + cn) <= (((p `1 ) / |.p.|) - cn) / (1 + cn) by A23, XREAL_1:74;
then A27: - 1 <= (((p `1 ) / |.p.|) - cn) / (1 + cn) by A26, XCMPLX_1:198;
(((p `1 ) / |.p.|) - cn) / (1 + cn) <= 1 by A21, A26;
then ((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 <= 1 ^2 by A27, SQUARE_1:119;
then A28: 1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ) >= 0 by XREAL_1:50;
A29: (qz `2 ) ^2 = (|.p.| ^2 ) * ((sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))) ^2 ) by A19
.= (|.p.| ^2 ) * (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 )) by A28, SQUARE_1:def 4 ;
|.qz.| ^2 = ((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) by JGRAPH_3:10
.= |.p.| ^2 by A19, A29 ;
then sqrt (|.qz.| ^2 ) = |.p.| by SQUARE_1:89;
hence |.((cn -FanMorphS ) . p).| = |.p.| by SQUARE_1:89; :: thesis: verum

end;

suppose 1 + cn < 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

then A30: - (1 + cn) > - 0 by XREAL_1:26;
0 + ((p `1 ) ^2 ) < ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by A17, SQUARE_1:74, XREAL_1:10;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) < (|.p.| ^2 ) / (|.p.| ^2 ) by A20, A22, XREAL_1:76;
then ((p `1 ) ^2 ) / (|.p.| ^2 ) < 1 by A20, XCMPLX_1:60;
then ((p `1 ) / |.p.|) ^2 < 1 by XCMPLX_1:77;
then - 1 < (p `1 ) / |.p.| by SQUARE_1:122;
then ((p `1 ) / |.p.|) - cn > (- 1) - cn by XREAL_1:11;
hence |.((cn -FanMorphS ) . p).| = |.p.| by A17, A30, XREAL_1:51; :: thesis: verum

end;

end;

end;

end;

end;

suppose p `2 >= 0 ; :: thesis: |.((cn -FanMorphS ) . p).| = |.p.|

hence |.((cn -FanMorphS ) . p).| = |.p.| by Th120; :: thesis: verum

end;

end;