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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))))]| ) )

then FanN cn,q = |.q.| * |[((((q `1 ) / |.q.|) - cn) / (1 - cn)),(sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))]| by A2, Def4
.= |[(|.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 -FanMorphN ) . 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 -FanMorphN ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))))]| ) ) by A3, Def5, Th57; :: thesis: verum

end;

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

then A5: (cn -FanMorphN ) . q = q by Th56;
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;
A10: sqrt (|.q.| ^2 ) = |.q.| by SQUARE_1:89;
A11: 1 - cn > 0 by A1, XREAL_1:151;
A12: |.q.| > 0 by A2, Lm1;
((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 A12, 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, A10, 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 A11, XCMPLX_1:60;
hence ( ( (q `1 ) / |.q.| >= cn & q `2 >= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))))]| ) ) by Th56, Th57; :: thesis: verum

end;

suppose A16: q `2 <= 0 ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 >= 0 & q <> 0. (TOP-REAL 2) implies (cn -FanMorphN ) . 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 -FanMorphN ) . 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;
A20: |.q.| > 0 by A15, Lm1;
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 A20, 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 -FanMorphN ) . 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 -FanMorphN ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))))]| ) ) by A1, A16, A18, A24, Th56, 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))))]| ) ) ; :: thesis: verum

end;

end;