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

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

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

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

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

then FanE sn,q = |.q.| * |[(sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))),((((q `2 ) / |.q.|) - sn) / (1 - sn))]| by A3, Def6
.= |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| by EUCLID:62 ;
hence ( ( (q `2 ) / |.q.| >= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| ) & ( (q `2 ) / |.q.| <= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| ) ) by A4, Def7, Th90; :: thesis: verum

end;

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

then A6: (sn -FanMorphE ) . q = q by Th89;
A7: |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by JGRAPH_3:10;
A8: 1 - sn > 0 by A2, XREAL_1:151;
A9: q `1 = 0 by A3, A5;
|.q.| <> 0 by A3, TOPRNS_1:25;
then |.q.| ^2 > 0 by SQUARE_1:74;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) = 1 ^2 by A7, A9, XCMPLX_1:60;
then ((q `2 ) / |.q.|) ^2 = 1 ^2 by XCMPLX_1:77;
then A10: sqrt (((q `2 ) / |.q.|) ^2 ) = 1 by SQUARE_1:89;

A11: now

assume q `2 < 0 ; :: thesis: contradiction
then - ((q `2 ) / |.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 `2 by A7, A9, A11, SQUARE_1:89;
then 1 = (q `2 ) / |.q.| by A3, TOPRNS_1:25, XCMPLX_1:60;
then (((q `2 ) / |.q.|) - sn) / (1 - sn) = 1 by A8, XCMPLX_1:60;
hence ( ( (q `2 ) / |.q.| >= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| ) & ( (q `2 ) / |.q.| <= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| ) ) by A2, A6, A9, A12, EUCLID:57, SQUARE_1:82, TOPRNS_1:25, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

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

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

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

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

end;

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

then A15: q `1 = 0 by A13;
A16: 1 + sn > 0 by A1, XREAL_1:150;
A17: |.q.| <> 0 by A13, TOPRNS_1:25;
1 > (q `2 ) / |.q.| by A2, A13, XXREAL_0:2;
then 1 * |.q.| > ((q `2 ) / |.q.|) * |.q.| by A17, XREAL_1:70;
then A18: ( |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) & |.q.| > q `2 ) by A13, JGRAPH_3:10, TOPRNS_1:25, XCMPLX_1:88;
then A19: |.q.| = - (q `2 ) by A15, SQUARE_1:109;
A20: q `2 = - |.q.| by A15, A18, SQUARE_1:109;
then - 1 = (q `2 ) / |.q.| by A13, TOPRNS_1:25, XCMPLX_1:198;
then (((q `2 ) / |.q.|) - sn) / (1 + sn) = (- (1 + sn)) / (1 + sn)
.= - 1 by A16, XCMPLX_1:198 ;
then |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| = q by A15, A19, EUCLID:57, SQUARE_1:82;
hence ( ( (q `2 ) / |.q.| >= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| ) & ( (q `2 ) / |.q.| <= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| ) ) by A1, A14, A17, A20, Th89, XCMPLX_1:198; :: thesis: verum

end;

end;

end;

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

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

end;

end;