let sn be Real; for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds
(sn -FanMorphE) . x in K0
let x, K0 be set ; ( - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } implies (sn -FanMorphE) . x in K0 )
assume A1:
( - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } )
; (sn -FanMorphE) . x in K0
then consider p being Point of (TOP-REAL 2) such that
A2:
p = x
and
A3:
p `1 >= 0
and
A4:
p <> 0. (TOP-REAL 2)
;
then A6:
|.p.| ^2 > 0
by SQUARE_1:12;
per cases
( (p `2) / |.p.| <= sn or (p `2) / |.p.| > sn )
;
suppose A7:
(p `2) / |.p.| <= sn
;
(sn -FanMorphE) . x in K0reconsider p9 =
(sn -FanMorphE) . p as
Point of
(TOP-REAL 2) ;
(sn -FanMorphE) . p = |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]|
by A1, A3, A4, A7, Th84;
then A8:
p9 `1 = |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))
by EUCLID:52;
A9:
|.p.| ^2 = ((p `1) ^2) + ((p `2) ^2)
by JGRAPH_3:1;
A10:
1
+ sn > 0
by A1, XREAL_1:148;
per cases
( p `1 = 0 or p `1 <> 0 )
;
suppose
p `1 <> 0
;
(sn -FanMorphE) . x in K0then
0 + ((p `2) ^2) < ((p `1) ^2) + ((p `2) ^2)
by SQUARE_1:12, XREAL_1:8;
then
((p `2) ^2) / (|.p.| ^2) < (|.p.| ^2) / (|.p.| ^2)
by A6, A9, XREAL_1:74;
then
((p `2) ^2) / (|.p.| ^2) < 1
by A6, XCMPLX_1:60;
then
((p `2) / |.p.|) ^2 < 1
by XCMPLX_1:76;
then
- 1
< (p `2) / |.p.|
by SQUARE_1:52;
then
(- 1) - sn < ((p `2) / |.p.|) - sn
by XREAL_1:9;
then
((- 1) * (1 + sn)) / (1 + sn) < (((p `2) / |.p.|) - sn) / (1 + sn)
by A10, XREAL_1:74;
then A11:
- 1
< (((p `2) / |.p.|) - sn) / (1 + sn)
by A10, XCMPLX_1:89;
((p `2) / |.p.|) - sn <= 0
by A7, XREAL_1:47;
then
1
^2 > ((((p `2) / |.p.|) - sn) / (1 + sn)) ^2
by A10, A11, SQUARE_1:50;
then
1
- (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2) > 0
by XREAL_1:50;
then
sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)) > 0
by SQUARE_1:25;
then
|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))) > 0
by A5, XREAL_1:129;
hence
(sn -FanMorphE) . x in K0
by A1, A2, A8, JGRAPH_2:3;
verum end; end; suppose A12:
(p `2) / |.p.| > sn
;
(sn -FanMorphE) . x in K0reconsider p9 =
(sn -FanMorphE) . p as
Point of
(TOP-REAL 2) ;
(sn -FanMorphE) . p = |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 - sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 - sn)))]|
by A1, A3, A4, A12, Th84;
then A13:
p9 `1 = |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 - sn)) ^2)))
by EUCLID:52;
A14:
|.p.| ^2 = ((p `1) ^2) + ((p `2) ^2)
by JGRAPH_3:1;
A15:
1
- sn > 0
by A1, XREAL_1:149;
per cases
( p `1 = 0 or p `1 <> 0 )
;
suppose
p `1 <> 0
;
(sn -FanMorphE) . x in K0then
0 + ((p `2) ^2) < ((p `1) ^2) + ((p `2) ^2)
by SQUARE_1:12, XREAL_1:8;
then
((p `2) ^2) / (|.p.| ^2) < (|.p.| ^2) / (|.p.| ^2)
by A6, A14, XREAL_1:74;
then
((p `2) ^2) / (|.p.| ^2) < 1
by A6, XCMPLX_1:60;
then
((p `2) / |.p.|) ^2 < 1
by XCMPLX_1:76;
then
(p `2) / |.p.| < 1
by SQUARE_1:52;
then
((p `2) / |.p.|) - sn < 1
- sn
by XREAL_1:9;
then
(((p `2) / |.p.|) - sn) / (1 - sn) < (1 - sn) / (1 - sn)
by A15, XREAL_1:74;
then A16:
(((p `2) / |.p.|) - sn) / (1 - sn) < 1
by A15, XCMPLX_1:60;
(
- (1 - sn) < - 0 &
((p `2) / |.p.|) - sn >= sn - sn )
by A12, A15, XREAL_1:9, XREAL_1:24;
then
((- 1) * (1 - sn)) / (1 - sn) < (((p `2) / |.p.|) - sn) / (1 - sn)
by A15, XREAL_1:74;
then
- 1
< (((p `2) / |.p.|) - sn) / (1 - sn)
by A15, XCMPLX_1:89;
then
1
^2 > ((((p `2) / |.p.|) - sn) / (1 - sn)) ^2
by A16, SQUARE_1:50;
then
1
- (((((p `2) / |.p.|) - sn) / (1 - sn)) ^2) > 0
by XREAL_1:50;
then
sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 - sn)) ^2)) > 0
by SQUARE_1:25;
then
p9 `1 > 0
by A5, A13, XREAL_1:129;
hence
(sn -FanMorphE) . x in K0
by A1, A2, JGRAPH_2:3;
verum end; end;