let seq be Complex_Sequence; :: thesis: ( seq is convergent iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p )

A1: now

assume seq is convergent ; :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p
then consider z being Element of COMPLEX such that
A2: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - z).| < p by COMSEQ_2:def 4;
let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p
then 0 < p / 2 ;
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
|.((seq . m) - z).| < p / 2 by A2;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.((seq . m) - (seq . n)).| < p )
assume n <= m ; :: thesis: |.((seq . m) - (seq . n)).| < p
then A4: |.((seq . m) - z).| < p / 2 by A3;
|.((seq . n) - z).| < p / 2 by A3;
then |.((seq . m) - z).| + |.((seq . n) - z).| < (p / 2) + (p / 2) by A4, XREAL_1:10;
then A5: |.((seq . m) - z).| + |.(z - (seq . n)).| < p by COMPLEX1:146;
|.((seq . m) - (seq . n)).| <= |.((seq . m) - z).| + |.(z - (seq . n)).| by COMPLEX1:149;
hence |.((seq . m) - (seq . n)).| < p by A5, XXREAL_0:2; :: thesis: verum

end;

now

assume A6: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p ; :: thesis: ( Re seq is convergent & Im seq is convergent & seq is convergent )
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Re seq) . m) - ((Re seq) . n)) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Re seq) . m) - ((Re seq) . n)) < p )
A7: p is Real by XREAL_0:def 1;
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Re seq) . m) - ((Re seq) . n)) < p
then consider n being Element of NAT such that
A8: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p by A6, A7;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs (((Re seq) . m) - ((Re seq) . n)) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((Re seq) . m) - ((Re seq) . n)) < p )
assume n <= m ; :: thesis: abs (((Re seq) . m) - ((Re seq) . n)) < p
then A9: |.((seq . m) - (seq . n)).| < p by A8;
Re ((seq . m) - (seq . n)) = (Re (seq . m)) - (Re (seq . n)) by COMPLEX1:48
.= ((Re seq) . m) - (Re (seq . n)) by Def3
.= ((Re seq) . m) - ((Re seq) . n) by Def3 ;
then abs (((Re seq) . m) - ((Re seq) . n)) <= |.((seq . m) - (seq . n)).| by Th13;
hence abs (((Re seq) . m) - ((Re seq) . n)) < p by A9, XXREAL_0:2; :: thesis: verum

end;

hence A10: Re seq is convergent by SEQ_4:58; :: thesis: ( Im seq is convergent & seq is convergent )
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Im seq) . m) - ((Im seq) . n)) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Im seq) . m) - ((Im seq) . n)) < p )
A11: p is Real by XREAL_0:def 1;
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Im seq) . m) - ((Im seq) . n)) < p
then consider n being Element of NAT such that
A12: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p by A6, A11;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs (((Im seq) . m) - ((Im seq) . n)) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((Im seq) . m) - ((Im seq) . n)) < p )
assume n <= m ; :: thesis: abs (((Im seq) . m) - ((Im seq) . n)) < p
then A13: |.((seq . m) - (seq . n)).| < p by A12;
Im ((seq . m) - (seq . n)) = (Im (seq . m)) - (Im (seq . n)) by COMPLEX1:48
.= ((Im seq) . m) - (Im (seq . n)) by Def4
.= ((Im seq) . m) - ((Im seq) . n) by Def4 ;
then abs (((Im seq) . m) - ((Im seq) . n)) <= |.((seq . m) - (seq . n)).| by Th13;
hence abs (((Im seq) . m) - ((Im seq) . n)) < p by A13, XXREAL_0:2; :: thesis: verum

end;

hence Im seq is convergent by SEQ_4:58; :: thesis: seq is convergent
hence seq is convergent by A10, Th42; :: thesis: verum

end;

hence ( seq is convergent iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p ) by A1; :: thesis: verum