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 Element of NAT holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ; :: thesis:
hence A2: c is convergent by Th38; :: thesis:
for p being Element of REAL st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p

let p be Element of REAL ; :: thesis:
assume A3: 0 < p ; :: thesis:
then consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
abs ((a . m) - (lim a)) < p / 2 by SEQ_2:def 7;
consider n2 being Element of NAT such that
A5: for m being Element of NAT st n2 <= m holds
abs ((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 Element of NAT such that
A6: n1 <= n and
A7: n2 <= n ;
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A8: n <= m ; :: thesis:
then n2 <= m by A7, XXREAL_0:2;
then A9: abs ((b . m) - (lim b)) < p / 2 by A5;
n1 <= m by A6, A8, XXREAL_0:2;
then abs ((a . m) - (lim a)) < p / 2 by A4;
then A10: (abs ((a . m) - (lim a))) + (abs ((b . m) - (lim b))) < (p / 2) + (p / 2) by A9, XREAL_1:10;
( Re (c . m) = a . m & Re g = lim a ) by A1, COMPLEX1:28;
then A11: Re ((c . m) - g) = (a . m) - (lim a) by COMPLEX1:48;
( Im (c . m) = b . m & Im g = lim b ) by A1, COMPLEX1:28;
then A12: Im ((c . m) - g) = (b . m) - (lim b) by COMPLEX1:48;
|.((c . m) - g).| <= (abs (Re ((c . m) - g))) + (abs (Im ((c . m) - g))) by Th12;
hence |.((c . m) - g).| < p by A10, A11, A12, XXREAL_0:2; :: thesis:

end;