let q be Point of (TOP-REAL 2); :: thesis: for cn being Real holds
( ( (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))))]| ) & ( q `2 <= 0 implies (cn -FanMorphN) . q = q ) )
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))))]| ) & ( q `2 <= 0 implies (cn -FanMorphN) . q = q ) )

hereby :: thesis: ( q `2 <= 0 implies (cn -FanMorphN) . q = q )

assume ( (q `1) / |.q.| >= cn & q `2 > 0 ) ; :: 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 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;

assume A1: q `2 <= 0 ; :: thesis: (cn -FanMorphN) . q = q
(cn -FanMorphN) . q = FanN (cn,q) by Def5;
hence (cn -FanMorphN) . q = q by A1, Def4; :: thesis: verum