let a, b be Real_Sequence; :: thesis: for c being Complex_Sequence st ( for n being Nat holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds
( ( a is convergent & b is convergent ) iff c is convergent )
let c be Complex_Sequence; :: thesis: ( ( for n being Nat holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ) implies ( ( a is convergent & b is convergent ) iff c is convergent ) )
assume A1: for n being Nat holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ; :: thesis: ( ( a is convergent & b is convergent ) iff c is convergent )
thus ( a is convergent & b is convergent implies c is convergent ) :: thesis: ( c is convergent implies ( a is convergent & b is convergent ) )

proof

assume that
A2: a is convergent and
A3: b is convergent ; :: thesis: c is convergent
consider a1 being Real such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((a . m) - a1).| < p by A2, SEQ_2:def 6;
consider b1 being Real such that
A5: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((b . m) - b1).| < p by A3, SEQ_2:def 6;
reconsider a1 = a1, b1 = b1 as Real ;
reconsider g = a1 + (b1 * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
take g ; :: according to COMSEQ_2:def 5 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((c . b₃) - g).| ) )
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

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((c . m) - g).| < p )
assume A6: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((c . m) - g).| < p
then consider n1 being Nat such that
A7: for m being Nat st n1 <= m holds
|.((a . m) - a1).| < p / 2 by A4;
consider n2 being Nat such that
A8: for m being Nat st n2 <= m holds
|.((b . m) - b1).| < p / 2 by A5, A6;
( n1 <= n1 + n2 & n2 <= n1 + n2 ) by NAT_1:11;
then consider n being Nat such that
A9: n1 <= n and
A10: n2 <= n ;
take n ; :: thesis: for m being Nat st n <= m holds
|.((c . m) - g).| < p
for m being Nat st n <= m holds
|.((c . m) - g).| < p

proof

let m be Nat; :: thesis: ( n <= m implies |.((c . m) - g).| < p )
( Re (c . m) = a . m & Re g = a1 ) by A1, COMPLEX1:12;
then A11: Re ((c . m) - g) = (a . m) - a1 by COMPLEX1:19;
( Im (c . m) = b . m & Im g = b1 ) by A1, COMPLEX1:12;
then A12: Im ((c . m) - g) = (b . m) - b1 by COMPLEX1:19;
assume A13: n <= m ; :: thesis: |.((c . m) - g).| < p
then n2 <= m by A10, XXREAL_0:2;
then A14: |.((b . m) - b1).| < p / 2 by A8;
n1 <= m by A9, A13, XXREAL_0:2;
then |.((a . m) - a1).| < p / 2 by A7;
then A15: |.((a . m) - a1).| + |.((b . m) - b1).| < (p / 2) + (p / 2) by A14, XREAL_1:8;
|.((c . m) - g).| <= |.(Re ((c . m) - g)).| + |.(Im ((c . m) - g)).| by Th12;
hence |.((c . m) - g).| < p by A15, A11, A12, XXREAL_0:2; :: thesis: verum

end;

hence for m being Nat st n <= m holds
|.((c . m) - g).| < p ; :: thesis: verum

end;

hence for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((c . b₃) - g).| ) ) ; :: thesis: verum

end;

assume c is convergent ; :: thesis: ( a is convergent & b is convergent )
then consider z being Complex such that
A16: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((c . m) - z).| < p ;
thus a is convergent :: thesis: b is convergent

proof

reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
take Re z ; :: according to COMSEQ_2:def 5 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((a . b₃) - (Re z)).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.((a . b₂) - (Re z)).| ) )
assume A17: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.((a . b₂) - (Re z)).| )
consider n being Nat such that
A18: for m being Nat st n <= m holds
|.((c . m) - z).| < p by A16, A17;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= |.((a . b₁) - (Re z)).| )
let m be Nat; :: thesis: ( not n <= m or not p <= |.((a . m) - (Re z)).| )
assume n <= m ; :: thesis: not p <= |.((a . m) - (Re z)).|
then A19: |.((c . m) - z).| < p by A18;
( Re (c . m) = a . m & Re ((c . m) - z) = (Re (c . m)) - (Re z) ) by A1, COMPLEX1:19;
then |.((a . m) - (Re z)).| <= |.((c . m) - z).| by Th13;
hence not p <= |.((a . m) - (Re z)).| by A19, XXREAL_0:2; :: thesis: verum

end;

take Im z ; :: according to COMSEQ_2:def 5 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((b . b₃) - (Im z)).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.((b . b₂) - (Im z)).| ) )
assume A20: p > 0 ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.((b . b₂) - (Im z)).| )
consider n being Nat such that
A21: for m being Nat st n <= m holds
|.((c . m) - z).| < p by A16, A20;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= |.((b . b₁) - (Im z)).| )
let m be Nat; :: thesis: ( not n <= m or not p <= |.((b . m) - (Im z)).| )
assume n <= m ; :: thesis: not p <= |.((b . m) - (Im z)).|
then A22: |.((c . m) - z).| < p by A21;
A23: Im ((c . m) - z) = (Im (c . m)) - (Im z) by COMPLEX1:19;
Im (c . m) = b . m by A1;
then |.((b . m) - (Im z)).| <= |.((c . m) - z).| by A23, Th13;
hence not p <= |.((b . m) - (Im z)).| by A22, XXREAL_0:2; :: thesis: verum