let X be Subset of COMPLEX; :: thesis: for z0 being Element of COMPLEX
for r being Real st X = { y where y is Complex : |.(y - z0).| <= r } holds
X is closed
let z0 be Element of COMPLEX ; :: thesis: for r being Real st X = { y where y is Complex : |.(y - z0).| <= r } holds
X is closed
let r be Real; :: thesis: ( X = { y where y is Complex : |.(y - z0).| <= r } implies X is closed )
reconsider X0 = X as Subset of COMPLEX ;
assume A1: X = { y where y is Complex : |.(y - z0).| <= r } ; :: thesis: X is closed
for s1 being Complex_Sequence st rng s1 c= X0 & s1 is convergent holds
lim s1 in X0

proof

reconsider r = r as Element of REAL by XREAL_0:def 1;
set s4 = seq_const r;
reconsider s2 = NAT --> z0 as Complex_Sequence ;
let s1 be Complex_Sequence; :: thesis: ( rng s1 c= X0 & s1 is convergent implies lim s1 in X0 )
assume that
A2: rng s1 c= X0 and
A3: s1 is convergent ; :: thesis: lim s1 in X0
set s3 = s1 - s2;
A4: s2 is convergent by CFCONT_1:26;
then A5: lim (s1 - s2) = (lim s1) - (lim s2) by A3, COMSEQ_2:26;
A6: for n being Element of NAT holds |.(s1 - s2).| . n <= r

proof

let n be Element of NAT ; :: thesis: |.(s1 - s2).| . n <= r

now :: thesis: for n being Element of NAT holds (s1 - s2) . n = (s1 . n) - z0

let n be Element of NAT ; :: thesis: (s1 - s2) . n = (s1 . n) - z0
(s1 - s2) . n = (s1 . n) + ((- s2) . n) by VALUED_1:1
.= (s1 . n) - (s2 . n) by VALUED_1:8 ;
hence (s1 - s2) . n = (s1 . n) - z0 ; :: thesis: verum

end;

then A7: (s1 - s2) . n = (s1 . n) - z0 ;
dom s1 = NAT by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 3;
then s1 . n in X0 by A2;
then ex y being Complex st
( y = s1 . n & |.(y - z0).| <= r ) by A1;
hence |.(s1 - s2).| . n <= r by A7, VALUED_1:18; :: thesis: verum

end;

s1 - s2 is convergent by A3, A4;
then A8: lim |.(s1 - s2).| = |.(lim (s1 - s2)).| by SEQ_2:27;
reconsider s3 = s1 - s2 as convergent Complex_Sequence by A3, A4;
A9: for n being Nat holds |.s3.| . n <= (seq_const r) . n

proof

let n be Nat; :: thesis: |.s3.| . n <= (seq_const r) . n
A10: n in NAT by ORDINAL1:def 12;
|.s3.| . n <= r by A6, A10;
hence |.s3.| . n <= (seq_const r) . n by SEQ_1:57; :: thesis: verum

end;

A11: for n being Element of NAT holds lim s2 = z0

proof

let n be Element of NAT ; :: thesis: lim s2 = z0
lim s2 = s2 . n by CFCONT_1:28
.= z0 ;
hence lim s2 = z0 ; :: thesis: verum

end;

lim (seq_const r) = (seq_const r) . 0 by SEQ_4:26
.= r by SEQ_1:57 ;
then lim |.s3.| <= r by A9, SEQ_2:18;
then |.((lim s1) - z0).| <= r by A11, A5, A8;
hence lim s1 in X0 by A1; :: thesis: verum

end;

hence X is closed ; :: thesis: verum