reconsider O = 0. (TOP-REAL 2) as Point of (Euclid 2) by EUCLID:67;
let cn be Real; :: thesis: for p2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 holds
ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (cn -FanMorphN) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (cn -FanMorphN) . p2 in V2 ) )
let p2 be Point of (TOP-REAL 2); :: thesis: ( - 1 < cn & cn < 1 implies ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (cn -FanMorphN) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (cn -FanMorphN) . p2 in V2 ) ) )
A1: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
then reconsider V0 = Ball (O,(|.p2.| + 1)) as Subset of (TOP-REAL 2) ;
( O in V0 & V0 c= cl_Ball (O,(|.p2.| + 1)) ) by GOBOARD6:1, METRIC_1:14;
then reconsider K0 = cl_Ball (O,(|.p2.| + 1)) as non empty compact Subset of (TOP-REAL 2) by A1, Th15;
set q3 = (cn -FanMorphN) . p2;
reconsider VV0 = V0 as Subset of (TopSpaceMetr (Euclid 2)) ;
reconsider u2 = p2 as Point of (Euclid 2) by EUCLID:67;
reconsider u3 = (cn -FanMorphN) . p2 as Point of (Euclid 2) by EUCLID:67;
A2: (cn -FanMorphN) .: K0 c= K0

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (cn -FanMorphN) .: K0 or y in K0 )
assume y in (cn -FanMorphN) .: K0 ; :: thesis: y in K0
then consider x being object such that
A3: x in dom (cn -FanMorphN) and
A4: x in K0 and
A5: y = (cn -FanMorphN) . x by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL 2) by A3;
reconsider uq = q as Point of (Euclid 2) by EUCLID:67;
dist (O,uq) <= |.p2.| + 1 by A4, METRIC_1:12;
then |.((0. (TOP-REAL 2)) - q).| <= |.p2.| + 1 by JGRAPH_1:28;
then |.(- q).| <= |.p2.| + 1 by RLVECT_1:4;
then A6: |.q.| <= |.p2.| + 1 by TOPRNS_1:26;
A7: y in rng (cn -FanMorphN) by A3, A5, FUNCT_1:def 3;
then reconsider u = y as Point of (Euclid 2) by EUCLID:67;
reconsider q4 = y as Point of (TOP-REAL 2) by A7;
|.q4.| = |.q.| by A5, Th66;
then |.(- q4).| <= |.p2.| + 1 by A6, TOPRNS_1:26;
then |.((0. (TOP-REAL 2)) - q4).| <= |.p2.| + 1 by RLVECT_1:4;
then dist (O,u) <= |.p2.| + 1 by JGRAPH_1:28;
hence y in K0 by METRIC_1:12; :: thesis: verum

end;

VV0 is open by TOPMETR:14;
then A8: V0 is open by Lm11, PRE_TOPC:30;
A9: |.p2.| < |.p2.| + 1 by XREAL_1:29;
then |.(- p2).| < |.p2.| + 1 by TOPRNS_1:26;
then |.((0. (TOP-REAL 2)) - p2).| < |.p2.| + 1 by RLVECT_1:4;
then dist (O,u2) < |.p2.| + 1 by JGRAPH_1:28;
then A10: p2 in V0 by METRIC_1:11;
|.((cn -FanMorphN) . p2).| = |.p2.| by Th66;
then |.(- ((cn -FanMorphN) . p2)).| < |.p2.| + 1 by A9, TOPRNS_1:26;
then |.((0. (TOP-REAL 2)) - ((cn -FanMorphN) . p2)).| < |.p2.| + 1 by RLVECT_1:4;
then dist (O,u3) < |.p2.| + 1 by JGRAPH_1:28;
then A11: (cn -FanMorphN) . p2 in V0 by METRIC_1:11;
assume A12: ( - 1 < cn & cn < 1 ) ; :: thesis: ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (cn -FanMorphN) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (cn -FanMorphN) . p2 in V2 ) )
K0 c= (cn -FanMorphN) .: K0

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in K0 or y in (cn -FanMorphN) .: K0 )
assume A13: y in K0 ; :: thesis: y in (cn -FanMorphN) .: K0
then reconsider q4 = y as Point of (TOP-REAL 2) ;
reconsider y = y as Point of (Euclid 2) by A13;
the carrier of (TOP-REAL 2) c= rng (cn -FanMorphN) by A12, Th72;
then q4 in rng (cn -FanMorphN) ;
then consider x being object such that
A14: x in dom (cn -FanMorphN) and
A15: y = (cn -FanMorphN) . x by FUNCT_1:def 3;
reconsider x = x as Point of (Euclid 2) by A14, Lm11;
reconsider q = x as Point of (TOP-REAL 2) by A14;
|.q4.| = |.q.| by A15, Th66;
then q in K0 by A13, Lm12;
hence y in (cn -FanMorphN) .: K0 by A14, A15, FUNCT_1:def 6; :: thesis: verum

end;

then K0 = (cn -FanMorphN) .: K0 by A2, XBOOLE_0:def 10;
hence ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (cn -FanMorphN) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (cn -FanMorphN) . p2 in V2 ) ) by A10, A8, A11, METRIC_1:14; :: thesis: verum