let a, b be convergent Real_Sequence; :: thesis:
let c be Complex_Sequence; :: thesis:
reconsider g = (lim a) + ((lim b) * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
assume A1: for n being Nat holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ; :: thesis:
hence A2: c is convergent by Th38; :: thesis:
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((c . m) - g).| < p

let p be Real; :: thesis:
assume A3: 0 < p ; :: thesis:
then consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
|.((a . m) - (lim a)).| < p / 2 by SEQ_2:def 7;
consider n2 being Nat such that
A5: for m being Nat st n2 <= m holds
|.((b . m) - (lim b)).| < p / 2 by A3, SEQ_2:def 7;
( n1 <= n1 + n2 & n2 <= n1 + n2 ) by NAT_1:11;
then consider n being Nat such that
A6: n1 <= n and
A7: n2 <= n ;
take n ; :: thesis:
let m be Nat; :: thesis:
assume A8: n <= m ; :: thesis:
then n2 <= m by A7, XXREAL_0:2;
then A9: |.((b . m) - (lim b)).| < p / 2 by A5;
n1 <= m by A6, A8, XXREAL_0:2;
then |.((a . m) - (lim a)).| < p / 2 by A4;
then A10: |.((a . m) - (lim a)).| + |.((b . m) - (lim b)).| < (p / 2) + (p / 2) by A9, XREAL_1:8;
( Re (c . m) = a . m & Re g = lim a ) by A1, COMPLEX1:12;
then A11: Re ((c . m) - g) = (a . m) - (lim a) by COMPLEX1:19;
( Im (c . m) = b . m & Im g = lim b ) by A1, COMPLEX1:12;
then A12: Im ((c . m) - g) = (b . m) - (lim b) by COMPLEX1:19;
|.((c . m) - g).| <= |.(Re ((c . m) - g)).| + |.(Im ((c . m) - g)).| by Th12;
hence |.((c . m) - g).| < p by A10, A11, A12, XXREAL_0:2; :: thesis:

end;