let cn be Real; :: thesis: for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds
(cn -FanMorphS) . x in K0
let x, K0 be set ; :: thesis: ( - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } implies (cn -FanMorphS) . x in K0 )
assume A1: ( - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: (cn -FanMorphS) . x in K0
then ex p being Point of (TOP-REAL 2) st
( p = x & p `2 >= 0 & p <> 0. (TOP-REAL 2) ) ;
hence (cn -FanMorphS) . x in K0 by A1, Th113; :: thesis: verum