let sn be Real; :: thesis: 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 -FanMorphW ) . x in K0
let x, K0 be set ; :: thesis: ( - 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 -FanMorphW ) . 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) ) } ) ; :: thesis: (sn -FanMorphW ) . x in K0
then consider p being Point of (TOP-REAL 2) such that
A2: ( p = x & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) ;

A3: now

assume |.p.| <= 0 ; :: thesis: contradiction
then |.p.| = 0 ;
hence contradiction by A2, TOPRNS_1:25; :: thesis: verum

end;

then A4: |.p.| ^2 > 0 by SQUARE_1:74;

per cases ( (p `2 ) / |.p.| <= sn or (p `2 ) / |.p.| > sn ) ;

suppose A5: (p `2 ) / |.p.| <= sn ; :: thesis: (sn -FanMorphW ) . x in K0

then A6: (sn -FanMorphW ) . p = |[(|.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 + sn)) ^2 ))))),(|.p.| * ((((p `2 ) / |.p.|) - sn) / (1 + sn)))]| by A1, A2, Th25;
reconsider p9 = (sn -FanMorphW ) . p as Point of (TOP-REAL 2) ;
A7: p9 `1 = |.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 + sn)) ^2 )))) by A6, EUCLID:56;
A8: 1 + sn > 0 by A1, XREAL_1:150;
A9: |.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by JGRAPH_3:10;

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

suppose p `1 = 0 ; :: thesis: (sn -FanMorphW ) . x in K0

hence (sn -FanMorphW ) . x in K0 by A1, A2, Th23; :: thesis: verum

end;

suppose p `1 <> 0 ; :: thesis: (sn -FanMorphW ) . x in K0

then 0 + ((p `2 ) ^2 ) < ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by SQUARE_1:74, XREAL_1:10;
then ((p `2 ) ^2 ) / (|.p.| ^2 ) < (|.p.| ^2 ) / (|.p.| ^2 ) by A4, A9, XREAL_1:76;
then ((p `2 ) ^2 ) / (|.p.| ^2 ) < 1 by A4, XCMPLX_1:60;
then A10: ((p `2 ) / |.p.|) ^2 < 1 by XCMPLX_1:77;
((p `2 ) / |.p.|) - sn <= 0 by A5, XREAL_1:49;
then A11: (((p `2 ) / |.p.|) - sn) / (1 + sn) < (1 + sn) / (1 + sn) by A8, XREAL_1:76;
- 1 < (p `2 ) / |.p.| by A10, SQUARE_1:122;
then (- 1) - sn < ((p `2 ) / |.p.|) - sn by XREAL_1:11;
then ((- 1) * (1 + sn)) / (1 + sn) < (((p `2 ) / |.p.|) - sn) / (1 + sn) by A8, XREAL_1:76;
then ( - 1 < (((p `2 ) / |.p.|) - sn) / (1 + sn) & (((p `2 ) / |.p.|) - sn) / (1 + sn) < 1 ) by A8, A11, XCMPLX_1:60, XCMPLX_1:90;
then 1 ^2 > ((((p `2 ) / |.p.|) - sn) / (1 + sn)) ^2 by SQUARE_1:120;
then 1 - (((((p `2 ) / |.p.|) - sn) / (1 + sn)) ^2 ) > 0 by XREAL_1:52;
then - (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 + sn)) ^2 )))) > 0 by SQUARE_1:93;
then - (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 + sn)) ^2 ))) < 0 ;
then |.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 + sn)) ^2 )))) < 0 by A3, XREAL_1:134;
hence (sn -FanMorphW ) . x in K0 by A1, A2, A7, JGRAPH_2:11; :: thesis: verum

end;

end;

end;

suppose A12: (p `2 ) / |.p.| > sn ; :: thesis: (sn -FanMorphW ) . x in K0

then A13: (sn -FanMorphW ) . p = |[(|.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 ))))),(|.p.| * ((((p `2 ) / |.p.|) - sn) / (1 - sn)))]| by A1, A2, Th25;
reconsider p9 = (sn -FanMorphW ) . p as Point of (TOP-REAL 2) ;
A14: p9 `1 = |.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 )))) by A13, EUCLID:56;
A15: 1 - sn > 0 by A1, XREAL_1:151;
A16: |.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by JGRAPH_3:10;

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

suppose p `1 = 0 ; :: thesis: (sn -FanMorphW ) . x in K0

hence (sn -FanMorphW ) . x in K0 by A1, A2, Th23; :: thesis: verum

end;

suppose p `1 <> 0 ; :: thesis: (sn -FanMorphW ) . x in K0

then 0 + ((p `2 ) ^2 ) < ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by SQUARE_1:74, XREAL_1:10;
then ((p `2 ) ^2 ) / (|.p.| ^2 ) < (|.p.| ^2 ) / (|.p.| ^2 ) by A4, A16, XREAL_1:76;
then ((p `2 ) ^2 ) / (|.p.| ^2 ) < 1 by A4, XCMPLX_1:60;
then ((p `2 ) / |.p.|) ^2 < 1 by XCMPLX_1:77;
then (p `2 ) / |.p.| < 1 by SQUARE_1:122;
then ((p `2 ) / |.p.|) - sn < 1 - sn by XREAL_1:11;
then A17: (((p `2 ) / |.p.|) - sn) / (1 - sn) < (1 - sn) / (1 - sn) by A15, XREAL_1:76;
A18: - (1 - sn) < - 0 by A15, XREAL_1:26;
((p `2 ) / |.p.|) - sn >= sn - sn by A12, XREAL_1:11;
then ((- 1) * (1 - sn)) / (1 - sn) < (((p `2 ) / |.p.|) - sn) / (1 - sn) by A15, A18, XREAL_1:76;
then ( - 1 < (((p `2 ) / |.p.|) - sn) / (1 - sn) & (((p `2 ) / |.p.|) - sn) / (1 - sn) < 1 ) by A15, A17, XCMPLX_1:60, XCMPLX_1:90;
then 1 ^2 > ((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 by SQUARE_1:120;
then 1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 ) > 0 by XREAL_1:52;
then - (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 )))) > 0 by SQUARE_1:93;
then - (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 ))) < 0 ;
then p9 `1 < 0 by A3, A14, XREAL_1:134;
hence (sn -FanMorphW ) . x in K0 by A1, A2, JGRAPH_2:11; :: thesis: verum

end;

end;

end;

end;