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 -FanMorphN ) . 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 -FanMorphN ) . 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 -FanMorphN ) . x in K0
then consider p being Point of (TOP-REAL 2) such that
A2: ( p = x & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) ;
thus (cn -FanMorphN ) . x in K0 by A1, A2, Th56; :: thesis: verum