let cn be Real; :: thesis: for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 < 0 & (q `1 ) / |.q.| > cn holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS ) . q holds
( p `2 < 0 & p `1 > 0 )
let q be Point of (TOP-REAL 2); :: thesis: ( - 1 < cn & cn < 1 & q `2 < 0 & (q `1 ) / |.q.| > cn implies for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS ) . q holds
( p `2 < 0 & p `1 > 0 ) )
assume that
A1: - 1 < cn and
A2: cn < 1 and
A3: q `2 < 0 and
A4: (q `1 ) / |.q.| > cn ; :: thesis: for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS ) . q holds
( p `2 < 0 & p `1 > 0 )
let p be Point of (TOP-REAL 2); :: thesis: ( p = (cn -FanMorphS ) . q implies ( p `2 < 0 & p `1 > 0 ) )
assume A5: p = (cn -FanMorphS ) . q ; :: thesis: ( p `2 < 0 & p `1 > 0 )

now

set q1 = |.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|;
set p1 = (1 / |.p.|) * p;
set p2 = (cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|);
( |[0 ,(- 1)]| `1 = 0 & |[0 ,(- 1)]| `2 = - 1 ) by EUCLID:56;
then A6: |.p.| * |[0 ,(- 1)]| = |[(|.p.| * 0 ),(|.p.| * (- 1))]| by EUCLID:61
.= |[0 ,(- |.p.|)]| ;
A7: ( |[cn,(- (sqrt (1 - (cn ^2 ))))]| `1 = cn & |[cn,(- (sqrt (1 - (cn ^2 ))))]| `2 = - (sqrt (1 - (cn ^2 ))) ) by EUCLID:56;
then A8: |.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]| = |[(|.p.| * cn),(|.p.| * (- (sqrt (1 - (cn ^2 )))))]| by EUCLID:61;
then A9: (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|) `1 = |.p.| * cn by EUCLID:56;
assume A10: p `1 = 0 ; :: thesis: contradiction
then |.p.| ^2 = ((p `2 ) ^2 ) + (0 ^2 ) by JGRAPH_3:10
.= (p `2 ) ^2 ;
then A11: ( p `2 = |.p.| or p `2 = - |.p.| ) by SQUARE_1:109;
then A12: |.p.| <> 0 by A2, A3, A4, A5, JGRAPH_4:144;
A13: (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|) `2 = - ((sqrt (1 - (cn ^2 ))) * |.p.|) by A8, EUCLID:56;
1 ^2 > cn ^2 by A1, A2, SQUARE_1:120;
then A14: 1 - (cn ^2 ) > 0 by XREAL_1:52;
then sqrt (1 - (cn ^2 )) > 0 by SQUARE_1:93;
then - (- ((sqrt (1 - (cn ^2 ))) * |.p.|)) > 0 by A12, XREAL_1:131;
then A15: (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|) `2 < 0 by A13;
A16: |.p.| * ((1 / |.p.|) * p) = (|.p.| * (1 / |.p.|)) * p by EUCLID:34
.= 1 * p by A12, XCMPLX_1:107
.= p by EUCLID:33 ;
A17: (1 / |.p.|) * p = |[((1 / |.p.|) * (p `1 )),((1 / |.p.|) * (p `2 ))]| by EUCLID:61;
then ((1 / |.p.|) * p) `2 = - (|.p.| * (1 / |.p.|)) by A2, A3, A4, A5, A11, EUCLID:56, JGRAPH_4:144
.= - 1 by A12, XCMPLX_1:107 ;
then A18: p = |.p.| * |[0 ,(- 1)]| by A10, A16, A17, EUCLID:56;
A19: |.(|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|).| = (abs |.p.|) * |.|[cn,(- (sqrt (1 - (cn ^2 ))))]|.| by TOPRNS_1:8
.= (abs |.p.|) * (sqrt ((cn ^2 ) + ((- (sqrt (1 - (cn ^2 )))) ^2 ))) by A7, JGRAPH_3:10
.= (abs |.p.|) * (sqrt ((cn ^2 ) + ((sqrt (1 - (cn ^2 ))) ^2 )))
.= (abs |.p.|) * (sqrt ((cn ^2 ) + (1 - (cn ^2 )))) by A14, SQUARE_1:def 4
.= |.p.| by ABSVALUE:def 1, SQUARE_1:83 ;
then A20: |.((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)).| = |.p.| by JGRAPH_4:135;
A21: ((|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|) `1 ) / |.(|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|).| = cn by A12, A9, A19, XCMPLX_1:90;
then A22: ((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)) `1 = 0 by A15, JGRAPH_4:149;
then |.((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)).| ^2 = ((((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)) `2 ) ^2 ) + (0 ^2 ) by JGRAPH_3:10
.= (((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)) `2 ) ^2 ;
then ( ((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)) `2 = |.((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)).| or ((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)) `2 = - |.((cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|)).| ) by SQUARE_1:109;
then A23: (cn -FanMorphS ) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]|) = |[0 ,(- |.p.|)]| by A15, A21, A22, A20, EUCLID:57, JGRAPH_4:149;
( cn -FanMorphS is one-to-one & dom (cn -FanMorphS ) = the carrier of (TOP-REAL 2) ) by A1, A2, FUNCT_2:def 1, JGRAPH_4:140;
then |.p.| * |[cn,(- (sqrt (1 - (cn ^2 ))))]| = q by A5, A18, A23, A6, FUNCT_1:def 8;
hence contradiction by A4, A12, A9, A19, XCMPLX_1:90; :: thesis: verum

end;

hence ( p `2 < 0 & p `1 > 0 ) by A2, A3, A4, A5, JGRAPH_4:144; :: thesis: verum