let q be Point of (TOP-REAL 2); :: thesis: for cn being Real st - 1 < cn & cn < 1 holds
( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )
let cn be Real; :: thesis: ( - 1 < cn & cn < 1 implies ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) ) )
assume A1: ( - 1 < cn & cn < 1 ) ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

per cases ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) ) or ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) ) or q `2 > 0 or q = 0. (TOP-REAL 2) ) ;

suppose A2: ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) ) ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

per cases ( q `2 < 0 or q `2 >= 0 ) ;

suppose A3: q `2 < 0 ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

then FanS cn,q = |.q.| * |[((((q `1 ) / |.q.|) - cn) / (1 - cn)),(- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 ))))]| by A2, Def8
.= |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| by EUCLID:62 ;
hence ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) ) by A3, Def9, Th121; :: thesis: verum

end;

suppose A4: q `2 >= 0 ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

then A5: (cn -FanMorphS ) . q = q by Th120;
A6: |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by JGRAPH_3:10;
A7: |.q.| <> 0 by A2, TOPRNS_1:25;
then A8: |.q.| ^2 > 0 by SQUARE_1:74;
A9: q `2 = 0 by A2, A4;
A11: sqrt (|.q.| ^2 ) = |.q.| by SQUARE_1:89;
A12: 1 - cn > 0 by A1, XREAL_1:151;
((q `1 ) ^2 ) / (|.q.| ^2 ) = 1 ^2 by A6, A8, A9, XCMPLX_1:60;
then ((q `1 ) / |.q.|) ^2 = 1 ^2 by XCMPLX_1:77;
then A13: sqrt (((q `1 ) / |.q.|) ^2 ) = 1 by SQUARE_1:89;

now

assume q `1 < 0 ; :: thesis: contradiction
then (q `1 ) / |.q.| < 0 by A7, XREAL_1:143;
then - ((q `1 ) / |.q.|) = 1 by A13, SQUARE_1:90;
hence contradiction by A1, A2; :: thesis: verum

end;

then A14: |.q.| = q `1 by A6, A9, A11, SQUARE_1:89;
then 1 = (q `1 ) / |.q.| by A2, TOPRNS_1:25, XCMPLX_1:60;
then (((q `1 ) / |.q.|) - cn) / (1 - cn) = 1 by A12, XCMPLX_1:60;
hence ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) ) by A1, A5, A7, A9, A14, EUCLID:57, SQUARE_1:82, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

suppose A15: ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) ) ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

per cases ( q `2 < 0 or q `2 >= 0 ) ;

suppose q `2 < 0 ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

hence ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) ) by Th120, Th121; :: thesis: verum

end;

suppose A16: q `2 >= 0 ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

A17: |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by JGRAPH_3:10;
A18: |.q.| <> 0 by A15, TOPRNS_1:25;
A19: q `2 = 0 by A15, A16;
A21: 1 + cn > 0 by A1, XREAL_1:150;
1 > (q `1 ) / |.q.| by A1, A15, XXREAL_0:2;
then 1 * |.q.| > ((q `1 ) / |.q.|) * |.q.| by A18, XREAL_1:70;
then A22: |.q.| > q `1 by A15, TOPRNS_1:25, XCMPLX_1:88;
then A23: |.q.| = - (q `1 ) by A17, A19, SQUARE_1:109;
A24: q `1 = - |.q.| by A17, A19, A22, SQUARE_1:109;
then - 1 = (q `1 ) / |.q.| by A15, TOPRNS_1:25, XCMPLX_1:198;
then (((q `1 ) / |.q.|) - cn) / (1 + cn) = (- (1 + cn)) / (1 + cn)
.= - 1 by A21, XCMPLX_1:198 ;
then |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| = q by A19, A23, EUCLID:57, SQUARE_1:82;
hence ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) ) by A1, A16, A18, A24, Th120, XCMPLX_1:198; :: thesis: verum

end;

end;

end;

suppose ( q `2 > 0 or q = 0. (TOP-REAL 2) ) ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) )

hence ( ( (q `1 ) / |.q.| >= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( (q `1 ) / |.q.| <= cn & q `2 <= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| ) ) ; :: thesis: verum

end;

end;