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

proof

let s1 be Complex_Sequence; :: thesis: ( rng s1 c= X0 & s1 is convergent implies lim s1 in X0 )
assume A2: ( rng s1 c= X0 & s1 is convergent ) ; :: thesis: lim s1 in X0
reconsider s2 = NAT --> z0 as Complex_Sequence ;
A3: s2 is convergent by CFCONT_1:48;
A4: 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:50
.= z0 by FUNCOP_1:13 ;
hence lim s2 = z0 ; :: thesis: verum

end;

set s3 = s1 - s2;
A5: ( s1 - s2 is convergent & lim (s1 - s2) = (lim s1) - (lim s2) ) by A2, A3, COMSEQ_2:25, COMSEQ_2:26;
then A6: ( s1 - s2 is convergent & lim |.(s1 - s2).| = |.(lim (s1 - s2)).| ) by COMSEQ_2:11;
A7: for n being Element of NAT holds |.(s1 - s2).| . n <= r

proof

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

proof

now

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 by FUNCOP_1:13; :: thesis: verum

end;

hence (s1 - s2) . n = (s1 . n) - z0 ; :: thesis: verum

end;

dom s1 = NAT by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 5;
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 A8, VALUED_1:18; :: thesis: verum

end;

reconsider s3 = s1 - s2 as convergent Complex_Sequence by A2, A3, COMSEQ_2:25;
reconsider s4 = NAT --> r as Real_Sequence ;
A11: lim s4 = s4 . 0 by SEQ_4:41
.= r by FUNCOP_1:13 ;
for n being Element of NAT holds |.s3.| . n <= s4 . n

proof

let n be Element of NAT ; :: thesis: |.s3.| . n <= s4 . n
|.s3.| . n <= r by A7;
hence |.s3.| . n <= s4 . n by FUNCOP_1:13; :: thesis: verum

end;

then lim |.s3.| <= r by A11, SEQ_2:32;
then |.((lim s1) - z0).| <= r by A6, A5, A4;
hence lim s1 in X0 by A1; :: thesis: verum

end;

hence X is closed by Def10; :: thesis: verum