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 A1: ( - 1 < cn & cn < 1 & q `2 < 0 & (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 A2: p = (cn -FanMorphS ) . q ; :: thesis: ( p `2 < 0 & p `1 > 0 )

now

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

end;

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