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

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

then FanW sn,q = |.q.| * |[(- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),((((q `2 ) / |.q.|) - sn) / (1 + sn))]| by A1, Def2
.= |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| by EUCLID:62 ;
hence (sn -FanMorphW ) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| by Def3; :: thesis: verum

end;

suppose A2: (q `2 ) / |.q.| = sn ; :: thesis: (sn -FanMorphW ) . 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 -FanMorphW ) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| by A1, A2, Th23; :: thesis: verum

end;

end;