theorem Th114: :: JGRAPH_4:114

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