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 that
A1: - 1 < cn and
A2: 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 A3: ( (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 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 FanS cn,q = |.q.| * |[((((q `1 ) / |.q.|) - cn) / (1 - cn)),(- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 ))))]| by A3, 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 A4, Def9, Th121; :: thesis: verum

end;

suppose A5: 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 A6: (cn -FanMorphS ) . q = q by Th120;
A7: |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by JGRAPH_3:10;
A8: 1 - cn > 0 by A2, XREAL_1:151;
A9: q `2 = 0 by A3, A5;
|.q.| <> 0 by A3, TOPRNS_1:25;
then |.q.| ^2 > 0 by SQUARE_1:74;
then ((q `1 ) ^2 ) / (|.q.| ^2 ) = 1 ^2 by A7, A9, XCMPLX_1:60;
then ((q `1 ) / |.q.|) ^2 = 1 ^2 by XCMPLX_1:77;
then A10: sqrt (((q `1 ) / |.q.|) ^2 ) = 1 by SQUARE_1:89;

A11: now

assume q `1 < 0 ; :: thesis: contradiction
then - ((q `1 ) / |.q.|) = 1 by A10, SQUARE_1:90;
hence contradiction by A1, A3; :: thesis: verum

end;

sqrt (|.q.| ^2 ) = |.q.| by SQUARE_1:89;
then A12: |.q.| = q `1 by A7, A9, A11, SQUARE_1:89;
then 1 = (q `1 ) / |.q.| by A3, TOPRNS_1:25, XCMPLX_1:60;
then (((q `1 ) / |.q.|) - cn) / (1 - cn) = 1 by A8, 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 A2, A6, A9, A12, EUCLID:57, SQUARE_1:82, TOPRNS_1:25, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

suppose A13: ( (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 A14: 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 A15: q `2 = 0 by A13;
A16: 1 + cn > 0 by A1, XREAL_1:150;
A17: |.q.| <> 0 by A13, TOPRNS_1:25;
1 > (q `1 ) / |.q.| by A2, A13, XXREAL_0:2;
then 1 * |.q.| > ((q `1 ) / |.q.|) * |.q.| by A17, XREAL_1:70;
then A18: ( |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) & |.q.| > q `1 ) by A13, JGRAPH_3:10, TOPRNS_1:25, XCMPLX_1:88;
then A19: |.q.| = - (q `1 ) by A15, SQUARE_1:109;
A20: q `1 = - |.q.| by A15, A18, SQUARE_1:109;
then - 1 = (q `1 ) / |.q.| by A13, TOPRNS_1:25, XCMPLX_1:198;
then (((q `1 ) / |.q.|) - cn) / (1 + cn) = (- (1 + cn)) / (1 + cn)
.= - 1 by A16, XCMPLX_1:198 ;
then |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| = q by A15, A19, 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, A14, A17, A20, 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;