theorem Th113: :: JGRAPH_4:113

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