theorem Th16: :: JGRAPH_4:16

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