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

then FanN (cn,q) = |.q.| * |[((((q `1) / |.q.|) - cn) / (1 + cn)),(sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))]| by A2, Def4
.= |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2))))]| by EUCLID:58 ;
hence (cn -FanMorphN) . q = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2))))]| by Def5; :: thesis: verum

end;

suppose A3: (q `1) / |.q.| = cn ; :: thesis: (cn -FanMorphN) . 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 -FanMorphN) . q = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2))))]| by A2, A3, Th49; :: thesis: verum

end;

end;