let q be Point of (TOP-REAL 2); :: thesis: for cn being real number holds
( ( (q `1 ) / |.q.| >= cn & q `2 < 0 implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( q `2 >= 0 implies (cn -FanMorphS ) . q = q ) )
let cn be real number ; :: thesis: ( ( (q `1 ) / |.q.| >= cn & q `2 < 0 implies (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| ) & ( q `2 >= 0 implies (cn -FanMorphS ) . q = q ) )
A1: (cn -FanMorphS ) . q = FanS cn,q by Def9;

hereby :: thesis: ( q `2 >= 0 implies (cn -FanMorphS ) . q = q )

assume ( (q `1 ) / |.q.| >= cn & q `2 < 0 ) ; :: thesis: (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]|
then FanS cn,q = |.q.| * |[((((q `1 ) / |.q.|) - cn) / (1 - cn)),(- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 ))))]| by Def8
.= |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| by EUCLID:62 ;
hence (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| by Def9; :: thesis: verum

end;

assume q `2 >= 0 ; :: thesis: (cn -FanMorphS ) . q = q
hence (cn -FanMorphS ) . q = q by A1, Def8; :: thesis: verum