let sn be Real; :: thesis: for q being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q `1 > 0 & (q `2 ) / |.q.| = sn holds
for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE ) . q holds
( p `1 > 0 & p `2 = 0 )
let q be Point of (TOP-REAL 2); :: thesis: ( - 1 < sn & sn < 1 & q `1 > 0 & (q `2 ) / |.q.| = sn implies for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE ) . q holds
( p `1 > 0 & p `2 = 0 ) )
assume A1: ( - 1 < sn & sn < 1 & q `1 > 0 & (q `2 ) / |.q.| = sn ) ; :: thesis: for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE ) . q holds
( p `1 > 0 & p `2 = 0 )
let p be Point of (TOP-REAL 2); :: thesis: ( p = (sn -FanMorphE ) . q implies ( p `1 > 0 & p `2 = 0 ) )
assume p = (sn -FanMorphE ) . q ; :: thesis: ( p `1 > 0 & p `2 = 0 )
then A3: p = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| by A1, Th89;
A4: |.q.| <> 0 by A1, JGRAPH_2:11, TOPRNS_1:25;
A5: ( p `1 = |.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))) & p `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)) ) by A3, EUCLID:56;
sqrt (1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 )) > 0 by A1, SQUARE_1:93;
hence ( p `1 > 0 & p `2 = 0 ) by A1, A4, A5, XREAL_1:131; :: thesis: verum