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

A1: now :: thesis: ( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p ) implies ( Re seq is convergent & Im seq is convergent & seq is convergent ) )

assume A2: for p being Real st 0 < p holds
ex n being Nat st
for m being 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 st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Re seq) . m) - ((Re seq) . n)).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Re seq) . m) - ((Re seq) . n)).| < p )
assume A3: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((Re seq) . m) - ((Re seq) . n)).| < p
consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p by A2, A3;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((Re seq) . m) - ((Re seq) . n)).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((Re seq) . m) - ((Re seq) . n)).| < p )
assume n <= m ; :: thesis: |.(((Re seq) . m) - ((Re seq) . n)).| < p
then A5: |.((seq . m) - (seq . n)).| < p by A4;
Re ((seq . m) - (seq . n)) = (Re (seq . m)) - (Re (seq . n)) by COMPLEX1:19
.= ((Re seq) . m) - (Re (seq . n)) by Def5
.= ((Re seq) . m) - ((Re seq) . n) by Def5 ;
then |.(((Re seq) . m) - ((Re seq) . n)).| <= |.((seq . m) - (seq . n)).| by Th13;
hence |.(((Re seq) . m) - ((Re seq) . n)).| < p by A5, XXREAL_0:2; :: thesis: verum

end;

hence A6: Re seq is convergent by SEQ_4:41; :: thesis: ( Im seq is convergent & seq is convergent )
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Im seq) . m) - ((Im seq) . n)).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Im seq) . m) - ((Im seq) . n)).| < p )
assume A7: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((Im seq) . m) - ((Im seq) . n)).| < p
consider n being Nat such that
A8: for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p by A2, A7;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((Im seq) . m) - ((Im seq) . n)).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((Im seq) . m) - ((Im seq) . n)).| < p )
assume n <= m ; :: thesis: |.(((Im seq) . m) - ((Im seq) . n)).| < p
then A9: |.((seq . m) - (seq . n)).| < p by A8;
Im ((seq . m) - (seq . n)) = (Im (seq . m)) - (Im (seq . n)) by COMPLEX1:19
.= ((Im seq) . m) - (Im (seq . n)) by Def6
.= ((Im seq) . m) - ((Im seq) . n) by Def6 ;
then |.(((Im seq) . m) - ((Im seq) . n)).| <= |.((seq . m) - (seq . n)).| by Th13;
hence |.(((Im seq) . m) - ((Im seq) . n)).| < p by A9, XXREAL_0:2; :: thesis: verum

end;

hence Im seq is convergent by SEQ_4:41; :: thesis: seq is convergent
hence seq is convergent by A6, Th42; :: thesis: verum

end;

now :: thesis: ( seq is convergent implies for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p )

assume seq is convergent ; :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p
then consider z being Complex such that
A10: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p
then consider n being Nat such that
A11: for m being Nat st n <= m holds
|.((seq . m) - z).| < p / 2 by A10;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (seq . n)).| < p )
assume n <= m ; :: thesis: |.((seq . m) - (seq . n)).| < p
then A12: |.((seq . m) - z).| < p / 2 by A11;
|.((seq . n) - z).| < p / 2 by A11;
then |.((seq . m) - z).| + |.((seq . n) - z).| < (p / 2) + (p / 2) by A12, XREAL_1:8;
then A13: |.((seq . m) - z).| + |.(z - (seq . n)).| < p by COMPLEX1:60;
|.((seq . m) - (seq . n)).| <= |.((seq . m) - z).| + |.(z - (seq . n)).| by COMPLEX1:63;
hence |.((seq . m) - (seq . n)).| < p by A13, XXREAL_0:2; :: thesis: verum

end;

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