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 ) ) )
assume A1: ( - 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 ) )
reconsider O = 0. (TOP-REAL 2) as Point of (Euclid 2) by EUCLID:71;
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) ;
A2: |.p2.| < |.p2.| + 1 by XREAL_1:31;
A3: O in V0 by GOBOARD6:4;
A4: V0 c= cl_Ball O,(|.p2.| + 1) by METRIC_1:15;
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
then reconsider K0 = cl_Ball O,(|.p2.| + 1) as non empty compact Subset of (TOP-REAL 2) by A3, A4, Th22;
reconsider u2 = p2 as Point of (Euclid 2) by EUCLID:71;
A5: (cn -FanMorphN ) .: K0 c= K0

proof

let y be set ; :: 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 set such that
A6: ( x in dom (cn -FanMorphN ) & x in K0 & y = (cn -FanMorphN ) . x ) by FUNCT_1:def 12;
reconsider q = x as Point of (TOP-REAL 2) by A6;
reconsider uq = q as Point of (Euclid 2) by EUCLID:71;
A7: y in rng (cn -FanMorphN ) by A6, FUNCT_1:def 5;
then reconsider u = y as Point of (Euclid 2) by EUCLID:71;
reconsider q4 = y as Point of (TOP-REAL 2) by A7;
A8: |.q4.| = |.q.| by A6, Th73;
dist O,uq <= |.p2.| + 1 by A6, METRIC_1:13;
then |.((0. (TOP-REAL 2)) - q).| <= |.p2.| + 1 by JGRAPH_1:45;
then |.((0. (TOP-REAL 2)) + (- q)).| <= |.p2.| + 1 by EUCLID:45;
then |.(- q).| <= |.p2.| + 1 by EUCLID:31;
then |.q.| <= |.p2.| + 1 by TOPRNS_1:27;
then |.(- q4).| <= |.p2.| + 1 by A8, TOPRNS_1:27;
then |.((0. (TOP-REAL 2)) + (- q4)).| <= |.p2.| + 1 by EUCLID:31;
then |.((0. (TOP-REAL 2)) - q4).| <= |.p2.| + 1 by EUCLID:45;
then dist O,u <= |.p2.| + 1 by JGRAPH_1:45;
hence y in K0 by METRIC_1:13; :: thesis: verum

end;

K0 c= (cn -FanMorphN ) .: K0

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in K0 or y in (cn -FanMorphN ) .: K0 )
assume A9: y in K0 ; :: thesis: y in (cn -FanMorphN ) .: K0
reconsider q4 = y as Point of (TOP-REAL 2) by A9;
reconsider y = y as Point of (Euclid 2) by A9, XX;
the carrier of (TOP-REAL 2) c= rng (cn -FanMorphN ) by A1, Th79;
then q4 in rng (cn -FanMorphN ) by TARSKI:def 3;
then consider x being set such that
A10: ( x in dom (cn -FanMorphN ) & y = (cn -FanMorphN ) . x ) by FUNCT_1:def 5;
reconsider x = x as Point of (Euclid 2) by A10, XX;
reconsider q = x as Point of (TOP-REAL 2) by A10;
|.q4.| = |.q.| by A10, Th73;
then q in K0 by A9, Lm11;
hence y in (cn -FanMorphN ) .: K0 by A10, FUNCT_1:def 12; :: thesis: verum

end;

then A11: K0 = (cn -FanMorphN ) .: K0 by A5, XBOOLE_0:def 10;
|.(- p2).| < |.p2.| + 1 by A2, TOPRNS_1:27;
then |.((0. (TOP-REAL 2)) + (- p2)).| < |.p2.| + 1 by EUCLID:31;
then |.((0. (TOP-REAL 2)) - p2).| < |.p2.| + 1 by EUCLID:45;
then dist O,u2 < |.p2.| + 1 by JGRAPH_1:45;
then A12: p2 in V0 by METRIC_1:12;
reconsider VV0 = V0 as Subset of (TopSpaceMetr (Euclid 2)) by XX;
VV0 is open by TOPMETR:21;
then A13: V0 is open by XX, PRE_TOPC:60;
set q3 = (cn -FanMorphN ) . p2;
reconsider u3 = (cn -FanMorphN ) . p2 as Point of (Euclid 2) by EUCLID:71;
|.((cn -FanMorphN ) . p2).| = |.p2.| by Th73;
then |.(- ((cn -FanMorphN ) . p2)).| < |.p2.| + 1 by A2, TOPRNS_1:27;
then |.((0. (TOP-REAL 2)) + (- ((cn -FanMorphN ) . p2))).| < |.p2.| + 1 by EUCLID:31;
then |.((0. (TOP-REAL 2)) - ((cn -FanMorphN ) . p2)).| < |.p2.| + 1 by EUCLID:45;
then dist O,u3 < |.p2.| + 1 by JGRAPH_1:45;
then (cn -FanMorphN ) . p2 in V0 by METRIC_1:12;
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 A11, A12, A13, METRIC_1:15; :: thesis: verum