let a, b be Real_Sequence; :: thesis: for c being convergent Complex_Sequence st ( for n being Element of NAT holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds
( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) )
let c be convergent Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ) implies ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) )
assume A1: for n being Element of NAT holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ; :: thesis: ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) )
then A2: ( a is convergent & b is convergent ) by Th38;
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((a . m) - (Re (lim c))) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((a . m) - (Re (lim c))) < p )
A4: p is Real by XREAL_0:def 1;
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((a . m) - (Re (lim c))) < p
then consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
|.((c . m) - (lim c)).| < p by A4, COMSEQ_2:def 5;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((a . m) - (Re (lim c))) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((a . m) - (Re (lim c))) < p )
assume n <= m ; :: thesis: abs ((a . m) - (Re (lim c))) < p
then A6: |.((c . m) - (lim c)).| < p by A5;
Re (c . m) = a . m by A1;
then Re ((c . m) - (lim c)) = (a . m) - (Re (lim c)) by COMPLEX1:48;
then abs ((a . m) - (Re (lim c))) <= |.((c . m) - (lim c)).| by Th13;
hence abs ((a . m) - (Re (lim c))) < p by A6, XXREAL_0:2; :: thesis: verum

end;

for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((b . m) - (Im (lim c))) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((b . m) - (Im (lim c))) < p )
A7: p is Real by XREAL_0:def 1;
assume p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((b . m) - (Im (lim c))) < p
then consider n being Element of NAT such that
A8: for m being Element of NAT st n <= m holds
|.((c . m) - (lim c)).| < p by A7, COMSEQ_2:def 5;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((b . m) - (Im (lim c))) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((b . m) - (Im (lim c))) < p )
assume n <= m ; :: thesis: abs ((b . m) - (Im (lim c))) < p
then A9: |.((c . m) - (lim c)).| < p by A8;
A10: Im (c . m) = b . m by A1;
Im ((c . m) - (lim c)) = (Im (c . m)) - (Im (lim c)) by COMPLEX1:48;
then abs ((b . m) - (Im (lim c))) <= |.((c . m) - (lim c)).| by A10, Th13;
hence abs ((b . m) - (Im (lim c))) < p by A9, XXREAL_0:2; :: thesis: verum

end;

hence ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) by A2, A3, SEQ_2:def 7; :: thesis: verum