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

proof

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

end;

hence lim c = (lim a) + ((lim b) * <i> ) by A2, COMSEQ_2:def 5; :: thesis: verum