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