theorem Th115: :: JGRAPH_4:115

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