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

now :: thesis: ( ( (q `2) / |.q.| < sn & (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| ) or ( (q `2) / |.q.| = sn & (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| ) )

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

case (q `2) / |.q.| < sn ; :: 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 A2, 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;

case A3: (q `2) / |.q.| = sn ; :: thesis: (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]|

then (((q `2) / |.q.|) - sn) / (1 - sn) = 0 ;
hence (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| by A2, A3, Th82; :: thesis: verum

end;

end;

end;

hence (sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| ; :: thesis: verum