theorem Th84: :: JGRAPH_4:84

for q being Point of (TOP-REAL 2)
for sn being Real st - 1 < sn & sn < 1 holds
( ( (q `2) / |.q.| >= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| ) & ( (q `2) / |.q.| <= sn & q `1 >= 0 & q <> 0. (TOP-REAL 2) implies (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| ) )