let q be Point of (TOP-REAL 2); :: thesis: for sn being Real holds
( ( (q `2) / |.q.| >= sn & q `1 > 0 implies (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| ) & ( q `1 <= 0 implies (sn -FanMorphE) . q = q ) )
let sn be Real; :: thesis: ( ( (q `2) / |.q.| >= sn & q `1 > 0 implies (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| ) & ( q `1 <= 0 implies (sn -FanMorphE) . q = q ) )

hereby :: thesis: ( q `1 <= 0 implies (sn -FanMorphE) . q = q )

assume ( (q `2) / |.q.| >= sn & q `1 > 0 ) ; :: thesis: (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]|
then FanE (sn,q) = |.q.| * |[(sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))),((((q `2) / |.q.|) - sn) / (1 - sn))]| by Def6
.= |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| by EUCLID:58 ;
hence (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| by Def7; :: thesis: verum

end;

assume A1: q `1 <= 0 ; :: thesis: (sn -FanMorphE) . q = q
(sn -FanMorphE) . q = FanE (sn,q) by Def7;
hence (sn -FanMorphE) . q = q by A1, Def6; :: thesis: verum