let a, b be Real_Sequence; :: thesis:
let c be convergent Complex_Sequence; :: thesis:
assume A1: for n being Nat holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ; :: thesis:
A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((b . m) - (Im (lim c))).| < p

let p be Real; :: thesis:
assume A3: p > 0 ; :: thesis:
consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((c . m) - (lim c)).| < p by A3, COMSEQ_2:def 6;
take n ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then A5: |.((c . m) - (lim c)).| < p by A4;
( Im (c . m) = b . m & Im ((c . m) - (lim c)) = (Im (c . m)) - (Im (lim c)) ) by A1, COMPLEX1:19;
then |.((b . m) - (Im (lim c))).| <= |.((c . m) - (lim c)).| by Th13;
hence |.((b . m) - (Im (lim c))).| < p by A5, XXREAL_0:2; :: thesis:

end;

A6: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((a . m) - (Re (lim c))).| < p

let p be Real; :: thesis:
assume A7: 0 < p ; :: thesis:
consider n being Nat such that
A8: for m being Nat st n <= m holds
|.((c . m) - (lim c)).| < p by A7, COMSEQ_2:def 6;
take n ; :: thesis:
let m be Nat; :: thesis:
Re (c . m) = a . m by A1;
then Re ((c . m) - (lim c)) = (a . m) - (Re (lim c)) by COMPLEX1:19;
then A9: |.((a . m) - (Re (lim c))).| <= |.((c . m) - (lim c)).| by Th13;
assume n <= m ; :: thesis:
then |.((c . m) - (lim c)).| < p by A8;
hence |.((a . m) - (Re (lim c))).| < p by A9, XXREAL_0:2; :: thesis:

end;