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