let q be Point of (TOP-REAL 2); 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; ( - 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
; ( ( (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) )
;
( ( (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 A5:
q `1 <= 0
;
( ( (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 Th82;
A7:
|.q.| ^2 = ((q `1) ^2) + ((q `2) ^2)
by JGRAPH_3:1;
A8:
1
- sn > 0
by A2, XREAL_1:149;
A9:
q `1 = 0
by A3, A5;
|.q.| <> 0
by A3, TOPRNS_1:24;
then
|.q.| ^2 > 0
by SQUARE_1:12;
then
((q `2) ^2) / (|.q.| ^2) = 1
^2
by A7, A9, XCMPLX_1:60;
then
((q `2) / |.q.|) ^2 = 1
^2
by XCMPLX_1:76;
then A10:
sqrt (((q `2) / |.q.|) ^2) = 1
by SQUARE_1:22;
sqrt (|.q.| ^2) = |.q.|
by SQUARE_1:22;
then A12:
|.q.| = q `2
by A7, A9, A11, SQUARE_1:22;
then
1
= (q `2) / |.q.|
by A3, TOPRNS_1:24, 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:53, SQUARE_1:17, TOPRNS_1:24, XCMPLX_1:60;
verum end; end; end; suppose A13:
(
(q `2) / |.q.| <= sn &
q `1 >= 0 &
q <> 0. (TOP-REAL 2) )
;
( ( (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 A14:
q `1 <= 0
;
( ( (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:148;
A17:
|.q.| <> 0
by A13, TOPRNS_1:24;
1
> (q `2) / |.q.|
by A2, A13, XXREAL_0:2;
then
1
* |.q.| > ((q `2) / |.q.|) * |.q.|
by A17, XREAL_1:68;
then A18:
(
|.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) &
|.q.| > q `2 )
by A13, JGRAPH_3:1, TOPRNS_1:24, XCMPLX_1:87;
then A19:
|.q.| = - (q `2)
by A15, SQUARE_1:40;
A20:
q `2 = - |.q.|
by A15, A18, SQUARE_1:40;
then
- 1
= (q `2) / |.q.|
by A13, TOPRNS_1:24, XCMPLX_1:197;
then (((q `2) / |.q.|) - sn) / (1 + sn) =
(- (1 + sn)) / (1 + sn)
.=
- 1
by A16, XCMPLX_1:197
;
then
|[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| = q
by A15, A19, EUCLID:53, SQUARE_1:17;
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, Th82, XCMPLX_1:197;
verum end; end; end; end;