let q be Point of (TOP-REAL 2); :: thesis: for sn being real number holds
( ( (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)))]| ) & ( q `1 >= 0 implies (sn -FanMorphW ) . q = q ) )
let sn be real number ; :: 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)))]| ) & ( q `1 >= 0 implies (sn -FanMorphW ) . q = q ) )

hereby :: thesis: ( q `1 >= 0 implies (sn -FanMorphW ) . q = q )

assume ( (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)))]|
then FanW sn,q = |.q.| * |[(- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),((((q `2 ) / |.q.|) - sn) / (1 - sn))]| by 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;

assume A1: q `1 >= 0 ; :: thesis: (sn -FanMorphW ) . q = q
(sn -FanMorphW ) . q = FanW sn,q by Def3;
hence (sn -FanMorphW ) . q = q by A1, Def2; :: thesis: verum