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

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

suppose A1: ( (q `2 ) / |.q.| >= sn & q `1 > 0 ) ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

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

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

suppose A7: 1 - sn = 0 ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

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

end;

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

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

suppose A10: 1 - sn > 0 ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

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

end;

suppose A15: 1 - sn < 0 ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

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

end;

end;

end;

end;

end;

suppose A17: ( (q `2 ) / |.q.| < sn & q `1 > 0 ) ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

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

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

suppose A24: 1 + sn = 0 ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

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

end;

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

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

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

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

end;

suppose 1 + sn < 0 ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

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

end;

end;

end;

end;

end;

suppose q `1 <= 0 ; :: thesis: |.((sn -FanMorphE ) . p).| = |.p.|

hence |.((sn -FanMorphE ) . p).| = |.p.| by Th89; :: thesis: verum

end;

end;