let sn be Real; :: thesis: for q being Point of (TOP-REAL 2) st 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: ( 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 that
A1: q `1 > 0 and
A2: (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 )
A3: ( |.q.| <> 0 & sqrt (1 - (((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2)) > 0 ) by A1, A2, JGRAPH_2:3, SQUARE_1:25, TOPRNS_1:24;
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 A4: p = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| by A1, A2, Th89;
then p `1 = |.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))) by EUCLID:52;
hence ( p `1 > 0 & p `2 = 0 ) by A2, A4, A3, EUCLID:52, XREAL_1:129; :: thesis: verum