let q be Point of (TOP-REAL 2); :: thesis: 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 )))))]|
let cn be Real; :: thesis: ( (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 )))))]| )
assume A1: ( (q `1 ) / |.q.| <= cn & q `2 < 0 ) ; :: thesis: (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]|

per cases ( (q `1 ) / |.q.| < cn or (q `1 ) / |.q.| = cn ) by A1, XXREAL_0:1;

suppose (q `1 ) / |.q.| < cn ; :: thesis: (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]|

then FanS cn,q = |.q.| * |[((((q `1 ) / |.q.|) - cn) / (1 + cn)),(- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))))]| by A1, Def8
.= |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| by EUCLID:62 ;
hence (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| by Def9; :: thesis: verum

end;

suppose A2: (q `1 ) / |.q.| = cn ; :: thesis: (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]|

then (((q `1 ) / |.q.|) - cn) / (1 - cn) = 0 ;
hence (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| by A1, A2, Th120; :: thesis: verum

end;

end;