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 :: thesis: not p `1 = 0

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:52;
then A6: |.p.| * |[0,(- 1)]| = |[(|.p.| * 0),(|.p.| * (- 1))]| by EUCLID:57
.= |[0,(- |.p.|)]| ;
A7: ( |[cn,(- (sqrt (1 - (cn ^2))))]| `1 = cn & |[cn,(- (sqrt (1 - (cn ^2))))]| `2 = - (sqrt (1 - (cn ^2))) ) by EUCLID:52;
then A8: |.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]| = |[(|.p.| * cn),(|.p.| * (- (sqrt (1 - (cn ^2)))))]| by EUCLID:57;
then A9: (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `1 = |.p.| * cn by EUCLID:52;
assume A10: p `1 = 0 ; :: thesis: contradiction
then |.p.| ^2 = ((p `2) ^2) + (0 ^2) by JGRAPH_3:1
.= (p `2) ^2 ;
then A11: ( p `2 = |.p.| or p `2 = - |.p.| ) by SQUARE_1:40;
then A12: |.p.| <> 0 by A2, A3, A4, A5, JGRAPH_4:137;
A13: (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `2 = - ((sqrt (1 - (cn ^2))) * |.p.|) by A8, EUCLID:52;
1 ^2 > cn ^2 by A1, A2, SQUARE_1:50;
then A14: 1 - (cn ^2) > 0 by XREAL_1:50;
then sqrt (1 - (cn ^2)) > 0 by SQUARE_1:25;
then - (- ((sqrt (1 - (cn ^2))) * |.p.|)) > 0 by A12, XREAL_1:129;
then A15: (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `2 < 0 by A13;
A16: |.p.| * ((1 / |.p.|) * p) = (|.p.| * (1 / |.p.|)) * p by RLVECT_1:def 7
.= 1 * p by A12, XCMPLX_1:106
.= p by RLVECT_1:def 8 ;
A17: (1 / |.p.|) * p = |[((1 / |.p.|) * (p `1)),((1 / |.p.|) * (p `2))]| by EUCLID:57;
then ((1 / |.p.|) * p) `2 = - (|.p.| * (1 / |.p.|)) by A2, A3, A4, A5, A11, EUCLID:52, JGRAPH_4:137
.= - 1 by A12, XCMPLX_1:106 ;
then A18: p = |.p.| * |[0,(- 1)]| by A10, A16, A17, EUCLID:52;
A19: |.(|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|).| = |.|.p.|.| * |.|[cn,(- (sqrt (1 - (cn ^2))))]|.| by TOPRNS_1:7
.= |.|.p.|.| * (sqrt ((cn ^2) + ((- (sqrt (1 - (cn ^2)))) ^2))) by A7, JGRAPH_3:1
.= |.|.p.|.| * (sqrt ((cn ^2) + ((sqrt (1 - (cn ^2))) ^2)))
.= |.|.p.|.| * (sqrt ((cn ^2) + (1 - (cn ^2)))) by A14, SQUARE_1:def 2
.= |.p.| by ABSVALUE:def 1 ;
then A20: |.((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)).| = |.p.| by JGRAPH_4:128;
A21: ((|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `1) / |.(|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|).| = cn by A12, A9, A19, XCMPLX_1:89;
then A22: ((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)) `1 = 0 by A15, JGRAPH_4:142;
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:1
.= (((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:40;
then A23: (cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) = |[0,(- |.p.|)]| by A15, A21, A22, A20, EUCLID:53, JGRAPH_4:142;
( cn -FanMorphS is one-to-one & dom (cn -FanMorphS) = the carrier of (TOP-REAL 2) ) by A1, A2, FUNCT_2:def 1, JGRAPH_4:133;
then |.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]| = q by A5, A18, A23, A6, FUNCT_1:def 4;
hence contradiction by A4, A12, A9, A19, XCMPLX_1:89; :: thesis: verum

end;

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