:: COMSEQ_3 semantic presentation

begin

             Lm1:  0c = 0 + (0 * <i>)
;

theorem :: COMSEQ_3:1
for n being Element of NAT holds
( n + 1 <> 0c & (n + 1) * <i> <> 0c ) ;

theorem Th2: :: COMSEQ_3:2
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq . n = 0 ) implies for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0 )
defpred S1[ Element of NAT ] means (abs rseq) . $1 = (Partial_Sums (abs rseq)) . $1;
assume A1: for n being Element of NAT holds rseq . n = 0 ; ::_thesis: for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
thus (abs rseq) . (k + 1) = 0 + ((abs rseq) . (k + 1))
.= (abs 0) + ((abs rseq) . (k + 1)) by ABSVALUE:def_1
.= (abs (rseq . k)) + ((abs rseq) . (k + 1)) by A1
.= ((Partial_Sums (abs rseq)) . k) + ((abs rseq) . (k + 1)) by A3, SEQ_1:12
.= (Partial_Sums (abs rseq)) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum
end;
let m be Element of NAT ; ::_thesis: (Partial_Sums (abs rseq)) . m = 0
A4: S1[ 0 ] by SERIES_1:def_1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence (Partial_Sums (abs rseq)) . m = (abs rseq) . m
.= abs (rseq . m) by SEQ_1:12
.= abs 0 by A1
.= 0 by ABSVALUE:def_1 ;
::_thesis: verum
end;

theorem Th3: :: COMSEQ_3:3
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
rseq is absolutely_summable
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq . n = 0 ) implies rseq is absolutely_summable )
assume A1: for n being Element of NAT holds rseq . n = 0 ; ::_thesis: rseq is absolutely_summable
take  0 ; :: according to SEQ_2:def_6,SERIES_1:def_2,SERIES_1:def_4 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs (((Partial_Sums (abs rseq)) . b3) - 0) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((Partial_Sums (abs rseq)) . b2) - 0) ) )
assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((Partial_Sums (abs rseq)) . b2) - 0) )
take  0 ; ::_thesis: for b1 being Element of NAT holds
( not 0 <= b1 or not p <= abs (((Partial_Sums (abs rseq)) . b1) - 0) )
let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= abs (((Partial_Sums (abs rseq)) . m) - 0) )
assume  0 <= m ; ::_thesis: not p <= abs (((Partial_Sums (abs rseq)) . m) - 0)
abs (((Partial_Sums (abs rseq)) . m) - 0) = abs (0 - 0) by A1, Th2
.= 0 by ABSVALUE:def_1 ;
hence  abs (((Partial_Sums (abs rseq)) . m) - 0) < p by A2; ::_thesis: verum
end;

reconsider C = NAT --> 0 as Real_Sequence by FUNCOP_1:45;

Lm2:  for n being Element of NAT holds C . n = 0
by FUNCOP_1:7;

registration
cluster Function-like V18( NAT , REAL ) summable  ->  convergent for Element of K19(K20(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is summable holds
b1 is convergent by SERIES_1:4;
end;

registration
cluster Function-like V18( NAT , REAL ) absolutely_summable  ->  summable for Element of K19(K20(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is absolutely_summable holds
b1 is summable ;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued absolutely_summable for Element of K19(K20(NAT,REAL));
existence
 ex b1 being Real_Sequence st b1 is absolutely_summable by Lm2, Th3;
end;

theorem :: COMSEQ_3:4
for rseq being Real_Sequence st rseq is convergent holds
for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p
proof
let rseq be Real_Sequence; ::_thesis: ( rseq is convergent implies for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p )
assume A1: rseq is convergent ; ::_thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p
then consider n being Element of NAT  such that
A2: for m being Element of NAT st n <= m holds
abs ((rseq . m) - (rseq . n)) < p / 2 by A1, SEQ_4:41;
take  n ; ::_thesis: for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p
now__::_thesis:_for_m,_l_being_Element_of_NAT_st_n_<=_m_&_n_<=_l_holds_
abs_((rseq_._m)_-_(rseq_._l))_<_p
let m, l be Element of NAT ; ::_thesis: ( n <= m & n <= l implies abs ((rseq . m) - (rseq . l)) < p )
assume  ( n <= m & n <= l ) ; ::_thesis: abs ((rseq . m) - (rseq . l)) < p
then  ( abs ((rseq . m) - (rseq . n)) < p / 2 & abs ((rseq . l) - (rseq . n)) < p / 2 ) by A2;
then A3: (abs ((rseq . m) - (rseq . n))) + (abs ((rseq . l) - (rseq . n))) < (p / 2) + (p / 2) by XREAL_1:8;
 abs ((rseq . m) - (rseq . l)) = abs (((rseq . m) - (rseq . n)) - ((rseq . l) - (rseq . n))) ;
then  abs ((rseq . m) - (rseq . l)) <= (abs ((rseq . m) - (rseq . n))) + (abs ((rseq . l) - (rseq . n))) by COMPLEX1:57;
hence  abs ((rseq . m) - (rseq . l)) < p by A3, XXREAL_0:2; ::_thesis: verum
end;
hence  for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p ; ::_thesis: verum
end;

theorem :: COMSEQ_3:5
for rseq being Real_Sequence
for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds
for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
proof
let rseq be Real_Sequence; ::_thesis: for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds
for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
let p be Real; ::_thesis: ( ( for n being Element of NAT holds rseq . n <= p ) implies for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l )
assume A1: for n being Element of NAT holds rseq . n <= p ; ::_thesis: for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
now__::_thesis:_for_n,_l_being_Element_of_NAT_holds_S1[l]
let n be Element of NAT ; ::_thesis: for l being Element of NAT holds S1[l]
defpred S1[ Element of NAT ] means ((Partial_Sums rseq) . (n + $1)) - ((Partial_Sums rseq) . n) <= p * $1;
A2: now__::_thesis:_for_l_being_Element_of_NAT_st_S1[l]_holds_
S1[l_+_1]
let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A3: S1[l] ; ::_thesis: S1[l + 1]
 rseq . ((n + l) + 1) <= p by A1;
then A4: (p * l) + (rseq . ((n + l) + 1)) <= (p * l) + p by XREAL_1:6;
((Partial_Sums rseq) . (n + (l + 1))) - ((Partial_Sums rseq) . n) = (((Partial_Sums rseq) . (n + l)) + (rseq . ((n + l) + 1))) - ((Partial_Sums rseq) . n) by SERIES_1:def_1
.= (((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n)) + (rseq . ((n + l) + 1)) ;
then  ((Partial_Sums rseq) . (n + (l + 1))) - ((Partial_Sums rseq) . n) <= (p * l) + (rseq . ((n + l) + 1)) by A3, XREAL_1:6;
hence  S1[l + 1] by A4, XXREAL_0:2; ::_thesis: verum
end;
A5: S1[ 0 ] ;
thus  for l being Element of NAT holds S1[l] from NAT_1:sch_1(A5, A2); ::_thesis: verum
end;
hence  for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l ; ::_thesis: verum
end;

theorem :: COMSEQ_3:6
for rseq being Real_Sequence
for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds
for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1)
proof
let rseq be Real_Sequence; ::_thesis: for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds
for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1)
let p be Real; ::_thesis: ( ( for n being Element of NAT holds rseq . n <= p ) implies for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1) )
defpred S1[ Element of NAT ] means (Partial_Sums rseq) . $1 <= p * ($1 + 1);
assume A1: for n being Element of NAT holds rseq . n <= p ; ::_thesis: for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1)
A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
 rseq . (n + 1) <= p by A1;
then A4: (p * (n + 1)) + (rseq . (n + 1)) <= (p * (n + 1)) + p by XREAL_1:6;
 (Partial_Sums rseq) . (n + 1) = ((Partial_Sums rseq) . n) + (rseq . (n + 1)) by SERIES_1:def_1;
then  (Partial_Sums rseq) . (n + 1) <= (p * (n + 1)) + (rseq . (n + 1)) by A3, XREAL_1:6;
hence  S1[n + 1] by A4, XXREAL_0:2; ::_thesis: verum
end;
 (Partial_Sums rseq) . 0 = rseq . 0 by SERIES_1:def_1;
then A5: S1[ 0 ] by A1;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); ::_thesis: verum
end;

theorem :: COMSEQ_3:7
for rseq1, rseq2 being Real_Sequence
for m being Element of NAT
for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)
proof
let rseq1, rseq2 be Real_Sequence; ::_thesis: for m being Element of NAT
for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)
let m be Element of NAT ; ::_thesis: for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)
let p be Real; ::_thesis: ( ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) implies (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) )
defpred S1[ Element of NAT ] means ( $1 <= m implies (Partial_Sums rseq1) . $1 <= p * ((Partial_Sums rseq2) . $1) );
assume A1: for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ; ::_thesis: (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)
A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_(_n_+_1_<=_m_implies_(Partial_Sums_rseq1)_._(n_+_1)_<=_p_*_((Partial_Sums_rseq2)_._(n_+_1))_)
assume A4: n + 1 <= m ; ::_thesis: (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1))
then  rseq1 . (n + 1) <= p * (rseq2 . (n + 1)) by A1;
then A5: (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) <= (p * ((Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1))) by XREAL_1:6;
 ( n < n + 1 & (Partial_Sums rseq1) . (n + 1) = ((Partial_Sums rseq1) . n) + (rseq1 . (n + 1)) ) by SERIES_1:def_1, XREAL_1:29;
then A6: (Partial_Sums rseq1) . (n + 1) <= (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) by A3, A4, XREAL_1:6, XXREAL_0:2;
(p * ((Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1))) = p * (((Partial_Sums rseq2) . n) + (rseq2 . (n + 1)))
.= p * ((Partial_Sums rseq2) . (n + 1)) by SERIES_1:def_1 ;
hence  (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1)) by A6, A5, XXREAL_0:2; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A7: S1[ 0 ]
proof
assume  0 <= m ; ::_thesis: (Partial_Sums rseq1) . 0 <= p * ((Partial_Sums rseq2) . 0)
 ( (Partial_Sums rseq1) . 0 = rseq1 . 0 & p * ((Partial_Sums rseq2) . 0) = p * (rseq2 . 0) ) by SERIES_1:def_1;
hence  (Partial_Sums rseq1) . 0 <= p * ((Partial_Sums rseq2) . 0) by A1; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2);
hence  (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) ; ::_thesis: verum
end;

theorem :: COMSEQ_3:8
for rseq1, rseq2 being Real_Sequence
for m being Element of NAT
for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
for n, l being Element of NAT st n + l <= m holds
((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))
proof
let rseq1, rseq2 be Real_Sequence; ::_thesis: for m being Element of NAT
for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
for n, l being Element of NAT st n + l <= m holds
((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))
let m be Element of NAT ; ::_thesis: for p being Real st ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
for n, l being Element of NAT st n + l <= m holds
((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))
let p be Real; ::_thesis: ( ( for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) implies for n, l being Element of NAT st n + l <= m holds
((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n)) )
assume A1: for n being Element of NAT st n <= m holds
rseq1 . n <= p * (rseq2 . n) ; ::_thesis: for n, l being Element of NAT st n + l <= m holds
((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))
let n be Element of NAT ; ::_thesis: for l being Element of NAT st n + l <= m holds
((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))
defpred S1[ Element of NAT ] means ( n + $1 <= m implies ((Partial_Sums rseq1) . (n + $1)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + $1)) - ((Partial_Sums rseq2) . n)) );
A2: for l being Element of NAT st S1[l] holds
S1[l + 1]
proof
let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A3: S1[l] ; ::_thesis: S1[l + 1]
assume A4: n + (l + 1) <= m ; ::_thesis: ((Partial_Sums rseq1) . (n + (l + 1))) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + (l + 1))) - ((Partial_Sums rseq2) . n))
then  ( (Partial_Sums rseq1) . (n + (l + 1)) = ((Partial_Sums rseq1) . (n + l)) + (rseq1 . ((n + l) + 1)) & rseq1 . ((n + l) + 1) <= p * (rseq2 . ((n + l) + 1)) ) by A1, SERIES_1:def_1;
then  (Partial_Sums rseq1) . (n + (l + 1)) <= ((Partial_Sums rseq1) . (n + l)) + (p * (rseq2 . ((n + l) + 1))) by XREAL_1:6;
then A5: ((Partial_Sums rseq1) . (n + (l + 1))) - ((Partial_Sums rseq1) . n) <= (((Partial_Sums rseq1) . (n + l)) + (p * (rseq2 . ((n + l) + 1)))) - ((Partial_Sums rseq1) . n) by XREAL_1:9;
 n + l < (n + l) + 1 by XREAL_1:29;
then A6: (((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n)) + (p * (rseq2 . ((n + l) + 1))) <= (p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))) + (p * (rseq2 . ((n + l) + 1))) by A3, A4, XREAL_1:6, XXREAL_0:2;
(p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))) + (p * (rseq2 . ((n + l) + 1))) = p * ((((Partial_Sums rseq2) . (n + l)) + (rseq2 . ((n + l) + 1))) - ((Partial_Sums rseq2) . n))
.= p * (((Partial_Sums rseq2) . (n + (l + 1))) - ((Partial_Sums rseq2) . n)) by SERIES_1:def_1 ;
hence  ((Partial_Sums rseq1) . (n + (l + 1))) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + (l + 1))) - ((Partial_Sums rseq2) . n)) by A5, A6, XXREAL_0:2; ::_thesis: verum
end;
A7: S1[ 0 ] ;
thus  for l being Element of NAT holds S1[l] from NAT_1:sch_1(A7, A2); ::_thesis: verum
end;

theorem :: COMSEQ_3:9
for rseq being Real_Sequence st ( for n being Element of NAT holds 0 <= rseq . n ) holds
( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) )
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= rseq . n ) implies ( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) )
assume A1: for n being Element of NAT holds 0 <= rseq . n ; ::_thesis: ( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) )
then A2: Partial_Sums rseq is non-decreasing by SERIES_1:16;
A3: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((Partial_Sums_rseq)_._m)_-_((Partial_Sums_rseq)_._n))_=_((Partial_Sums_rseq)_._m)_-_((Partial_Sums_rseq)_._n)
let n, m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) )
assume  n <= m ; ::_thesis: abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)
then  (Partial_Sums rseq) . n <= (Partial_Sums rseq) . m by A2, SEQM_3:6;
then  ((Partial_Sums rseq) . n) - ((Partial_Sums rseq) . n) <= ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by XREAL_1:9;
hence  abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by ABSVALUE:def_1; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_((Partial_Sums_rseq)_._n)_=_(Partial_Sums_rseq)_._n
let n be Element of NAT ; ::_thesis: abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n
A4: (Partial_Sums rseq) . 0 <= (Partial_Sums rseq) . n by A2, SEQM_3:6;
 ( (Partial_Sums rseq) . 0 = rseq . 0 & 0 <= rseq . 0 ) by A1, SERIES_1:def_1;
hence  abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n by A4, ABSVALUE:def_1; ::_thesis: verum
end;
hence  ( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) by A3; ::_thesis: verum
end;

theorem :: COMSEQ_3:10
for seq1, seq2 being Complex_Sequence st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c holds
lim seq1 = lim seq2
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c implies lim seq1 = lim seq2 )
assume that
A1: ( seq1 is convergent & seq2 is convergent ) and
A2: lim (seq1 - seq2) = 0c ; ::_thesis: lim seq1 = lim seq2
 lim (seq1 - seq2) = (lim seq1) - (lim seq2) by A1, COMSEQ_2:26;
hence  lim seq1 = lim seq2 by A2; ::_thesis: verum
end;

begin

   Lm3:  for seq being Complex_Sequence
for n being Element of NAT holds
( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
proof
let seq be Complex_Sequence; ::_thesis: for n being Element of NAT holds
( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
let n be Element of NAT ; ::_thesis: ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
 |.(seq . n).| = |.seq.| . n by VALUED_1:18;
hence  ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n ) by COMPLEX1:46; ::_thesis: verum
end;

definition
let z be complex number ;
funcz GeoSeq  ->  Complex_Sequence means :Def1: :: COMSEQ_3:def 1
( it . 0 = 1r & ( for n being Element of NAT holds it . (n + 1) = (it . n) * z ) );
existence
 ex b1 being Complex_Sequence st
( b1 . 0 = 1r & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) )
proof
reconsider z9 = z as Element of COMPLEX by XCMPLX_0:def_2;
deffunc H1( set , Element of COMPLEX ) ->  Element of COMPLEX = $2 * z9;
consider f being Function of NAT,COMPLEX such that
A1: ( f . 0 = 1r & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_12();
take  f ; ::_thesis: ( f . 0 = 1r & ( for n being Element of NAT holds f . (n + 1) = (f . n) * z ) )
thus  ( f . 0 = 1r & ( for n being Element of NAT holds f . (n + 1) = (f . n) * z ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Complex_Sequence st b1 . 0 = 1r & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) & b2 . 0 = 1r & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) holds
b1 = b2
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 . 0 = 1r & ( for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z ) & seq2 . 0 = 1r & ( for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ) implies seq1 = seq2 )
assume that
A2: seq1 . 0 = 1r and
A3: for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z and
A4: seq2 . 0 = 1r and
A5: for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ; ::_thesis: seq1 = seq2
defpred S1[ Element of NAT ] means seq1 . $1 = seq2 . $1;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
hence seq1 . (k + 1) = (seq2 . k) * z by A3
.= seq2 . (k + 1) by A5 ;
::_thesis: verum
end;
A7: S1[ 0 ] by A2, A4;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6);
hence  seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines GeoSeq COMSEQ_3:def_1_:_
 for z being complex number
for b2 being Complex_Sequence holds
( b2 = z GeoSeq iff ( b2 . 0 = 1r & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) ) );

notation
let z be complex number ;
let n be natural number ;
synonym z #N n for z |^ n;
end;

definition
let z be complex number ;
let n be natural number ;
:: original: #N
redefine funcz #N n ->  Element of COMPLEX  equals :: COMSEQ_3:def 2
(z GeoSeq) . n;
coherence
 z #N n is Element of COMPLEX by XCMPLX_0:def_2;
compatibility
 for b1 being Element of COMPLEX holds
( b1 = z #N n iff b1 = (z GeoSeq) . n )
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
defpred S1[ Element of NAT ] means z |^ $1 = (z GeoSeq) . $1;
let w be Element of COMPLEX ; ::_thesis: ( w = z #N n iff w = (z GeoSeq) . n )
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
hence z |^ (n + 1) = ((z GeoSeq) . n) * z by NEWTON:6
.= (z GeoSeq) . (n + 1) by Def1 ;
::_thesis: verum
end;
z |^ 0 = 1r by COMPLEX1:def_4, NEWTON:4
.= (z GeoSeq) . 0 by Def1 ;
then A2: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1);
then  z |^ n = (z GeoSeq) . n ;
hence  ( w = z #N n iff w = (z GeoSeq) . n ) ; ::_thesis: verum
end;
end;

:: deftheorem  defines #N COMSEQ_3:def_2_:_
 for z being complex number
for n being natural number holds z #N n = (z GeoSeq) . n;

theorem :: COMSEQ_3:11
for z being Element of COMPLEX holds z #N 0 = 1r by COMPLEX1:def_4, NEWTON:4;

definition
let f be complex-valued Function;
set A = dom f;
deffunc H1( set ) ->  Element of REAL = Re (f . $1);
func Re f ->  Function means :Def3: :: COMSEQ_3:def 3
( dom it = dom f & ( for x being set st x in dom it holds
it . x = Re (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = Re (f . x) ) )
proof
 ex f being Function st
( dom f = dom f & ( for x being set st x in dom f holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = Re (f . x) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = Re (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 . x = Re (f . x) ) holds
b1 = b2
proof
let g, h be Function; ::_thesis: ( dom g = dom f & ( for x being set st x in dom g holds
g . x = Re (f . x) ) & dom h = dom f & ( for x being set st x in dom h holds
h . x = Re (f . x) ) implies g = h )
assume that
A1: dom g = dom f and
A2: for x being set st x in dom g holds
g . x = H1(x) and
A3: dom h = dom f and
A4: for x being set st x in dom h holds
h . x = H1(x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_=_h_._x
let x be set ; ::_thesis: ( x in dom g implies g . x = h . x )
assume A5: x in dom g ; ::_thesis: g . x = h . x
hence g . x = H1(x) by A2
.= h . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence  g = h by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
deffunc H2( set ) ->  Element of REAL = Im (f . $1);
func Im f ->  Function means :Def4: :: COMSEQ_3:def 4
( dom it = dom f & ( for x being set st x in dom it holds
it . x = Im (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = Im (f . x) ) )
proof
 ex f being Function st
( dom f = dom f & ( for x being set st x in dom f holds
f . x = H2(x) ) ) from FUNCT_1:sch_3();
hence  ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = Im (f . x) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = Im (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 . x = Im (f . x) ) holds
b1 = b2
proof
let g, h be Function; ::_thesis: ( dom g = dom f & ( for x being set st x in dom g holds
g . x = Im (f . x) ) & dom h = dom f & ( for x being set st x in dom h holds
h . x = Im (f . x) ) implies g = h )
assume that
A6: dom g = dom f and
A7: for x being set st x in dom g holds
g . x = H2(x) and
A8: dom h = dom f and
A9: for x being set st x in dom h holds
h . x = H2(x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_=_h_._x
let x be set ; ::_thesis: ( x in dom g implies g . x = h . x )
assume A10: x in dom g ; ::_thesis: g . x = h . x
hence g . x = H2(x) by A7
.= h . x by A6, A8, A9, A10 ;
::_thesis: verum
end;
hence  g = h by A6, A8, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Re COMSEQ_3:def_3_:_
 for f being complex-valued Function
for b2 being Function holds
( b2 = Re f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 . x = Re (f . x) ) ) );

:: deftheorem Def4 defines Im COMSEQ_3:def_4_:_
 for f being complex-valued Function
for b2 being Function holds
( b2 = Im f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 . x = Im (f . x) ) ) );

registration
let f be complex-valued Function;
cluster Re f ->  real-valued ;
coherence
 Re f is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (Re f) or (Re f) . x is real )
assume  x in dom (Re f) ; ::_thesis: (Re f) . x is real
then  (Re f) . x = Re (f . x) by Def3;
hence  (Re f) . x is real ; ::_thesis: verum
end;
cluster Im f ->  real-valued ;
coherence
 Im f is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (Im f) or (Im f) . x is real )
assume  x in dom (Im f) ; ::_thesis: (Im f) . x is real
then  (Im f) . x = Im (f . x) by Def4;
hence  (Im f) . x is real ; ::_thesis: verum
end;
end;

definition
let X be set ;
let f be PartFunc of X,COMPLEX;
:: original: Re
redefine func Re f ->  PartFunc of X,REAL;
coherence
 Re f is PartFunc of X,REAL
proof
A1: dom f c= X by RELAT_1:def_18;
A2: rng (Re f) c= REAL by VALUED_0:def_3;
 dom (Re f) = dom f by Def3;
hence  Re f is PartFunc of X,REAL by A1, A2, RELSET_1:4; ::_thesis: verum
end;
:: original: Im
redefine func Im f ->  PartFunc of X,REAL;
coherence
 Im f is PartFunc of X,REAL
proof
A3: dom f c= X by RELAT_1:def_18;
A4: rng (Im f) c= REAL by VALUED_0:def_3;
 dom (Im f) = dom f by Def4;
hence  Im f is PartFunc of X,REAL by A3, A4, RELSET_1:4; ::_thesis: verum
end;
end;

definition
let c be Complex_Sequence;
:: original: Re
redefine func Re c ->  Real_Sequence means :Def5: :: COMSEQ_3:def 5
 for n being Element of NAT holds it . n = Re (c . n);
coherence
 Re c is Real_Sequence
proof
dom (Re c) = dom c by Def3
.= NAT by FUNCT_2:def_1 ;
then  Re c is total by PARTFUN1:def_2;
hence  Re c is Real_Sequence ; ::_thesis: verum
end;
compatibility
 for b1 being Real_Sequence holds
( b1 = Re c iff for n being Element of NAT holds b1 . n = Re (c . n) )
proof
let f be Real_Sequence; ::_thesis: ( f = Re c iff for n being Element of NAT holds f . n = Re (c . n) )
A1: dom (Re c) = dom c by Def3;
A2: dom c = NAT by FUNCT_2:def_1;
A3: dom f = NAT by FUNCT_2:def_1;
hence  ( f = Re c implies for n being Element of NAT holds f . n = Re (c . n) ) by Def3; ::_thesis: ( ( for n being Element of NAT holds f . n = Re (c . n) ) implies f = Re c )
assume A4: for n being Element of NAT holds f . n = Re (c . n) ; ::_thesis: f = Re c
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_(Re_c)_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = (Re c) . x )
assume A5: x in dom f ; ::_thesis: f . x = (Re c) . x
hence f . x = Re (c . x) by A3, A4
.= (Re c) . x by A1, A2, A3, A5, Def3 ;
::_thesis: verum
end;
hence  f = Re c by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
end;
:: original: Im
redefine func Im c ->  Real_Sequence means :Def6: :: COMSEQ_3:def 6
 for n being Element of NAT holds it . n = Im (c . n);
coherence
 Im c is Real_Sequence
proof
dom (Im c) = dom c by Def4
.= NAT by FUNCT_2:def_1 ;
then  Im c is total by PARTFUN1:def_2;
hence  Im c is Real_Sequence ; ::_thesis: verum
end;
compatibility
 for b1 being Real_Sequence holds
( b1 = Im c iff for n being Element of NAT holds b1 . n = Im (c . n) )
proof
let f be Real_Sequence; ::_thesis: ( f = Im c iff for n being Element of NAT holds f . n = Im (c . n) )
A6: dom (Im c) = dom c by Def4;
A7: dom c = NAT by FUNCT_2:def_1;
A8: dom f = NAT by FUNCT_2:def_1;
hence  ( f = Im c implies for n being Element of NAT holds f . n = Im (c . n) ) by Def4; ::_thesis: ( ( for n being Element of NAT holds f . n = Im (c . n) ) implies f = Im c )
assume A9: for n being Element of NAT holds f . n = Im (c . n) ; ::_thesis: f = Im c
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_(Im_c)_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = (Im c) . x )
assume A10: x in dom f ; ::_thesis: f . x = (Im c) . x
hence f . x = Im (c . x) by A8, A9
.= (Im c) . x by A6, A7, A8, A10, Def4 ;
::_thesis: verum
end;
hence  f = Im c by A6, A7, A8, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Re COMSEQ_3:def_5_:_
 for c being Complex_Sequence
for b2 being Real_Sequence holds
( b2 = Re c iff for n being Element of NAT holds b2 . n = Re (c . n) );

:: deftheorem Def6 defines Im COMSEQ_3:def_6_:_
 for c being Complex_Sequence
for b2 being Real_Sequence holds
( b2 = Im c iff for n being Element of NAT holds b2 . n = Im (c . n) );

theorem Th12: :: COMSEQ_3:12
for z being Element of COMPLEX holds |.z.| <= (abs (Re z)) + (abs (Im z))
proof
let z be Element of COMPLEX ; ::_thesis: |.z.| <= (abs (Re z)) + (abs (Im z))
 z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
then A1: |.z.| <= |.((Re z) + (0 * <i>)).| + |.(0 + ((Im z) * <i>)).| by COMPLEX1:56;
 ( Re (0 + ((Im z) * <i>)) = 0 & Im (0 + ((Im z) * <i>)) = Im z ) by COMPLEX1:12;
hence  |.z.| <= (abs (Re z)) + (abs (Im z)) by A1, COMPLEX1:51; ::_thesis: verum
end;

theorem Th13: :: COMSEQ_3:13
for z being Element of COMPLEX holds
( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| )
proof
let z be Element of COMPLEX ; ::_thesis: ( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| )
 0 <= (Re z) ^2 by XREAL_1:63;
then A1: 0 + ((Im z) ^2) <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:6;
 0 <= (Im z) ^2 by XREAL_1:63;
then A2: sqrt ((Im z) ^2) <= sqrt (((Re z) ^2) + ((Im z) ^2)) by A1, SQUARE_1:26;
 0 <= (Im z) ^2 by XREAL_1:63;
then A3: 0 + ((Re z) ^2) <= ((Im z) ^2) + ((Re z) ^2) by XREAL_1:6;
 0 <= (Re z) ^2 by XREAL_1:63;
then  ( |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2)) & sqrt ((Re z) ^2) <= sqrt (((Re z) ^2) + ((Im z) ^2)) ) by A3, COMPLEX1:def_12, SQUARE_1:26;
hence  ( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| ) by A2, COMPLEX1:72; ::_thesis: verum
end;

theorem Th14: :: COMSEQ_3:14
for seq1, seq2 being Complex_Sequence st Re seq1 = Re seq2 & Im seq1 = Im seq2 holds
seq1 = seq2
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( Re seq1 = Re seq2 & Im seq1 = Im seq2 implies seq1 = seq2 )
assume that
A1: Re seq1 = Re seq2 and
A2: Im seq1 = Im seq2 ; ::_thesis: seq1 = seq2
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n
let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n
A3: Im (seq1 . n) = (Im seq2) . n by A2, Def6
.= Im (seq2 . n) by Def6 ;
Re (seq1 . n) = (Re seq2) . n by A1, Def5
.= Re (seq2 . n) by Def5 ;
hence  seq1 . n = seq2 . n by A3, COMPLEX1:3; ::_thesis: verum
end;
hence  seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;

theorem Th15: :: COMSEQ_3:15
for seq1, seq2 being Complex_Sequence holds
( (Re seq1) + (Re seq2) = Re (seq1 + seq2) & (Im seq1) + (Im seq2) = Im (seq1 + seq2) )
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( (Re seq1) + (Re seq2) = Re (seq1 + seq2) & (Im seq1) + (Im seq2) = Im (seq1 + seq2) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Re_seq1)_+_(Re_seq2))_._n_=_(Re_(seq1_+_seq2))_._n
let n be Element of NAT ; ::_thesis: ((Re seq1) + (Re seq2)) . n = (Re (seq1 + seq2)) . n
thus ((Re seq1) + (Re seq2)) . n = ((Re seq1) . n) + ((Re seq2) . n) by SEQ_1:7
.= (Re (seq1 . n)) + ((Re seq2) . n) by Def5
.= (Re (seq1 . n)) + (Re (seq2 . n)) by Def5
.= Re ((seq1 . n) + (seq2 . n)) by COMPLEX1:8
.= Re ((seq1 + seq2) . n) by VALUED_1:1
.= (Re (seq1 + seq2)) . n by Def5 ; ::_thesis: verum
end;
hence  (Re seq1) + (Re seq2) = Re (seq1 + seq2) by FUNCT_2:63; ::_thesis: (Im seq1) + (Im seq2) = Im (seq1 + seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Im_seq1)_+_(Im_seq2))_._n_=_(Im_(seq1_+_seq2))_._n
let n be Element of NAT ; ::_thesis: ((Im seq1) + (Im seq2)) . n = (Im (seq1 + seq2)) . n
thus ((Im seq1) + (Im seq2)) . n = ((Im seq1) . n) + ((Im seq2) . n) by SEQ_1:7
.= (Im (seq1 . n)) + ((Im seq2) . n) by Def6
.= (Im (seq1 . n)) + (Im (seq2 . n)) by Def6
.= Im ((seq1 . n) + (seq2 . n)) by COMPLEX1:8
.= Im ((seq1 + seq2) . n) by VALUED_1:1
.= (Im (seq1 + seq2)) . n by Def6 ; ::_thesis: verum
end;
hence  (Im seq1) + (Im seq2) = Im (seq1 + seq2) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th16: :: COMSEQ_3:16
for seq being Complex_Sequence holds
( - (Re seq) = Re (- seq) & - (Im seq) = Im (- seq) )
proof
let seq be Complex_Sequence; ::_thesis: ( - (Re seq) = Re (- seq) & - (Im seq) = Im (- seq) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_(Re_seq))_._n_=_(Re_(-_seq))_._n
let n be Element of NAT ; ::_thesis: (- (Re seq)) . n = (Re (- seq)) . n
thus (- (Re seq)) . n = - ((Re seq) . n) by SEQ_1:10
.= - (Re (seq . n)) by Def5
.= Re (- (seq . n)) by COMPLEX1:17
.= Re ((- seq) . n) by VALUED_1:8
.= (Re (- seq)) . n by Def5 ; ::_thesis: verum
end;
hence  - (Re seq) = Re (- seq) by FUNCT_2:63; ::_thesis: - (Im seq) = Im (- seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_(Im_seq))_._n_=_(Im_(-_seq))_._n
let n be Element of NAT ; ::_thesis: (- (Im seq)) . n = (Im (- seq)) . n
thus (- (Im seq)) . n = - ((Im seq) . n) by SEQ_1:10
.= - (Im (seq . n)) by Def6
.= Im (- (seq . n)) by COMPLEX1:17
.= Im ((- seq) . n) by VALUED_1:8
.= (Im (- seq)) . n by Def6 ; ::_thesis: verum
end;
hence  - (Im seq) = Im (- seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th17: :: COMSEQ_3:17
for r being Real
for z being Element of COMPLEX holds
( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) )
proof
let r be Real; ::_thesis: for z being Element of COMPLEX holds
( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) )
let z be Element of COMPLEX ; ::_thesis: ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) )
reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def_2;
 r = r + (0 * <i>) ;
then A1: ( Re r = r & Im r = 0 ) by COMPLEX1:12;
r * z = (((Re r9) * (Re z)) - ((Im r9) * (Im z))) + ((((Re r9) * (Im z)) + ((Re z) * (Im r9))) * <i>) by COMPLEX1:def_6
.= (r * (Re z)) + ((r * (Im z)) * <i>) by A1 ;
hence  ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) ) by COMPLEX1:12; ::_thesis: verum
end;

theorem Th18: :: COMSEQ_3:18
for seq1, seq2 being Complex_Sequence holds
( (Re seq1) - (Re seq2) = Re (seq1 - seq2) & (Im seq1) - (Im seq2) = Im (seq1 - seq2) )
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( (Re seq1) - (Re seq2) = Re (seq1 - seq2) & (Im seq1) - (Im seq2) = Im (seq1 - seq2) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Re_seq1)_-_(Re_seq2))_._n_=_(Re_(seq1_-_seq2))_._n
let n be Element of NAT ; ::_thesis: ((Re seq1) - (Re seq2)) . n = (Re (seq1 - seq2)) . n
thus ((Re seq1) - (Re seq2)) . n = ((Re seq1) . n) + ((- (Re seq2)) . n) by SEQ_1:7
.= ((Re seq1) . n) + ((Re (- seq2)) . n) by Th16
.= ((Re seq1) + (Re (- seq2))) . n by SEQ_1:7
.= (Re (seq1 - seq2)) . n by Th15 ; ::_thesis: verum
end;
hence  (Re seq1) - (Re seq2) = Re (seq1 - seq2) by FUNCT_2:63; ::_thesis: (Im seq1) - (Im seq2) = Im (seq1 - seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Im_seq1)_-_(Im_seq2))_._n_=_(Im_(seq1_-_seq2))_._n
let n be Element of NAT ; ::_thesis: ((Im seq1) - (Im seq2)) . n = (Im (seq1 - seq2)) . n
thus ((Im seq1) - (Im seq2)) . n = ((Im seq1) . n) + ((- (Im seq2)) . n) by SEQ_1:7
.= ((Im seq1) . n) + ((Im (- seq2)) . n) by Th16
.= ((Im seq1) + (Im (- seq2))) . n by SEQ_1:7
.= (Im (seq1 - seq2)) . n by Th15 ; ::_thesis: verum
end;
hence  (Im seq1) - (Im seq2) = Im (seq1 - seq2) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_3:19
for seq being Complex_Sequence
for r being Real holds
( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )
proof
let seq be Complex_Sequence; ::_thesis: for r being Real holds
( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )
let r be Real; ::_thesis: ( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(Re_seq))_._n_=_(Re_(r_(#)_seq))_._n
let n be Element of NAT ; ::_thesis: (r (#) (Re seq)) . n = (Re (r (#) seq)) . n
thus (r (#) (Re seq)) . n = r * ((Re seq) . n) by SEQ_1:9
.= r * (Re (seq . n)) by Def5
.= Re (r * (seq . n)) by Th17
.= Re ((r (#) seq) . n) by VALUED_1:6
.= (Re (r (#) seq)) . n by Def5 ; ::_thesis: verum
end;
hence  r (#) (Re seq) = Re (r (#) seq) by FUNCT_2:63; ::_thesis: r (#) (Im seq) = Im (r (#) seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(Im_seq))_._n_=_(Im_(r_(#)_seq))_._n
let n be Element of NAT ; ::_thesis: (r (#) (Im seq)) . n = (Im (r (#) seq)) . n
thus (r (#) (Im seq)) . n = r * ((Im seq) . n) by SEQ_1:9
.= r * (Im (seq . n)) by Def6
.= Im (r * (seq . n)) by Th17
.= Im ((r (#) seq) . n) by VALUED_1:6
.= (Im (r (#) seq)) . n by Def6 ; ::_thesis: verum
end;
hence  r (#) (Im seq) = Im (r (#) seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_3:20
for seq being Complex_Sequence
for z being Element of COMPLEX holds
( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )
proof
let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX holds
( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )
let z be Element of COMPLEX ; ::_thesis: ( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_(z_(#)_seq))_._n_=_(((Re_z)_(#)_(Re_seq))_-_((Im_z)_(#)_(Im_seq)))_._n
let n be Element of NAT ; ::_thesis: (Re (z (#) seq)) . n = (((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq))) . n
thus (Re (z (#) seq)) . n = Re ((z (#) seq) . n) by Def5
.= Re (z * (seq . n)) by VALUED_1:6
.= Re ((((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n)))) + ((((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z))) * <i>)) by COMPLEX1:def_6
.= ((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n))) by COMPLEX1:12
.= ((Re z) * ((Re seq) . n)) - ((Im z) * (Im (seq . n))) by Def5
.= ((Re z) * ((Re seq) . n)) - ((Im z) * ((Im seq) . n)) by Def6
.= (((Re z) (#) (Re seq)) . n) - ((Im z) * ((Im seq) . n)) by SEQ_1:9
.= (((Re z) (#) (Re seq)) . n) - (((Im z) (#) (Im seq)) . n) by SEQ_1:9
.= (((Re z) (#) (Re seq)) . n) + (- (((Im z) (#) (Im seq)) . n))
.= (((Re z) (#) (Re seq)) . n) + ((- ((Im z) (#) (Im seq))) . n) by SEQ_1:10
.= (((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq))) . n by SEQ_1:7 ; ::_thesis: verum
end;
hence  Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) by FUNCT_2:63; ::_thesis: Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_(z_(#)_seq))_._n_=_(((Re_z)_(#)_(Im_seq))_+_((Im_z)_(#)_(Re_seq)))_._n
let n be Element of NAT ; ::_thesis: (Im (z (#) seq)) . n = (((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))) . n
thus (Im (z (#) seq)) . n = Im ((z (#) seq) . n) by Def6
.= Im (z * (seq . n)) by VALUED_1:6
.= Im ((((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n)))) + ((((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z))) * <i>)) by COMPLEX1:def_6
.= ((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z)) by COMPLEX1:12
.= ((Re z) * (Im (seq . n))) + ((Im z) * ((Re seq) . n)) by Def5
.= ((Re z) * ((Im seq) . n)) + ((Im z) * ((Re seq) . n)) by Def6
.= (((Re z) (#) (Im seq)) . n) + ((Im z) * ((Re seq) . n)) by SEQ_1:9
.= (((Re z) (#) (Im seq)) . n) + (((Im z) (#) (Re seq)) . n) by SEQ_1:9
.= (((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))) . n by SEQ_1:7 ; ::_thesis: verum
end;
hence  Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_3:21
for seq1, seq2 being Complex_Sequence holds
( Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) & Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) )
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) & Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_(seq1_(#)_seq2))_._n_=_(((Re_seq1)_(#)_(Re_seq2))_-_((Im_seq1)_(#)_(Im_seq2)))_._n
let n be Element of NAT ; ::_thesis: (Re (seq1 (#) seq2)) . n = (((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2))) . n
thus (Re (seq1 (#) seq2)) . n = Re ((seq1 (#) seq2) . n) by Def5
.= Re ((seq1 . n) * (seq2 . n)) by VALUED_1:5
.= Re ((((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n)))) + ((((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n)))) * <i>)) by COMPLEX1:def_6
.= ((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n))) by COMPLEX1:12
.= (((Re seq1) . n) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n))) by Def5
.= (((Re seq1) . n) * ((Re seq2) . n)) - ((Im (seq1 . n)) * (Im (seq2 . n))) by Def5
.= (((Re seq1) . n) * ((Re seq2) . n)) - ((Im (seq1 . n)) * ((Im seq2) . n)) by Def6
.= (((Re seq1) . n) * ((Re seq2) . n)) - (((Im seq1) . n) * ((Im seq2) . n)) by Def6
.= (((Re seq1) (#) (Re seq2)) . n) - (((Im seq1) . n) * ((Im seq2) . n)) by SEQ_1:8
.= (((Re seq1) (#) (Re seq2)) . n) - (((Im seq1) (#) (Im seq2)) . n) by SEQ_1:8
.= (((Re seq1) (#) (Re seq2)) . n) + (- (((Im seq1) (#) (Im seq2)) . n))
.= (((Re seq1) (#) (Re seq2)) . n) + ((- ((Im seq1) (#) (Im seq2))) . n) by SEQ_1:10
.= (((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2))) . n by SEQ_1:7 ; ::_thesis: verum
end;
hence  Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) by FUNCT_2:63; ::_thesis: Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2))
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_(seq1_(#)_seq2))_._n_=_(((Re_seq1)_(#)_(Im_seq2))_+_((Im_seq1)_(#)_(Re_seq2)))_._n
let n be Element of NAT ; ::_thesis: (Im (seq1 (#) seq2)) . n = (((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2))) . n
thus (Im (seq1 (#) seq2)) . n = Im ((seq1 (#) seq2) . n) by Def6
.= Im ((seq1 . n) * (seq2 . n)) by VALUED_1:5
.= Im ((((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n)))) + ((((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n)))) * <i>)) by COMPLEX1:def_6
.= ((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n))) by COMPLEX1:12
.= ((Re (seq1 . n)) * (Im (seq2 . n))) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def5
.= (((Re seq1) . n) * (Im (seq2 . n))) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def5
.= (((Re seq1) . n) * ((Im seq2) . n)) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def6
.= (((Re seq1) . n) * ((Im seq2) . n)) + (((Im seq1) . n) * ((Re seq2) . n)) by Def6
.= (((Re seq1) (#) (Im seq2)) . n) + (((Im seq1) . n) * ((Re seq2) . n)) by SEQ_1:8
.= (((Re seq1) (#) (Im seq2)) . n) + (((Im seq1) (#) (Re seq2)) . n) by SEQ_1:8
.= (((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2))) . n by SEQ_1:7 ; ::_thesis: verum
end;
hence  Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) by FUNCT_2:63; ::_thesis: verum
end;

definition
let Nseq be increasing sequence of NAT;
let seq be Complex_Sequence;
:: original: (#)
redefine funcseq * Nseq ->  Complex_Sequence;
coherence
 Nseq (#) seq is Complex_Sequence
proof
 dom (seq * Nseq) = NAT by FUNCT_2:def_1;
hence  Nseq (#) seq is Complex_Sequence ; ::_thesis: verum
end;
end;

theorem Th22: :: COMSEQ_3:22
for seq being Complex_Sequence
for Nseq being increasing sequence of NAT holds
( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq )
proof
let seq be Complex_Sequence; ::_thesis: for Nseq being increasing sequence of NAT holds
( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq )
let Nseq be increasing sequence of NAT; ::_thesis: ( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_(seq_*_Nseq))_._n_=_((Re_seq)_*_Nseq)_._n
let n be Element of NAT ; ::_thesis: (Re (seq * Nseq)) . n = ((Re seq) * Nseq) . n
thus (Re (seq * Nseq)) . n = Re ((seq * Nseq) . n) by Def5
.= Re (seq . (Nseq . n)) by FUNCT_2:15
.= (Re seq) . (Nseq . n) by Def5
.= ((Re seq) * Nseq) . n by FUNCT_2:15 ; ::_thesis: verum
end;
hence  Re (seq * Nseq) = (Re seq) * Nseq by FUNCT_2:63; ::_thesis: Im (seq * Nseq) = (Im seq) * Nseq
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_(seq_*_Nseq))_._n_=_((Im_seq)_*_Nseq)_._n
let n be Element of NAT ; ::_thesis: (Im (seq * Nseq)) . n = ((Im seq) * Nseq) . n
thus (Im (seq * Nseq)) . n = Im ((seq * Nseq) . n) by Def6
.= Im (seq . (Nseq . n)) by FUNCT_2:15
.= (Im seq) . (Nseq . n) by Def6
.= ((Im seq) * Nseq) . n by FUNCT_2:15 ; ::_thesis: verum
end;
hence  Im (seq * Nseq) = (Im seq) * Nseq by FUNCT_2:63; ::_thesis: verum
end;

theorem Th23: :: COMSEQ_3:23
for seq being Complex_Sequence
for k being Element of NAT holds
( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) )
proof
let seq be Complex_Sequence; ::_thesis: for k being Element of NAT holds
( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) )
let k be Element of NAT ; ::_thesis: ( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_((Re_seq)_^\_k)_._n_=_(Re_(seq_^\_k))_._n_&_((Im_seq)_^\_k)_._n_=_(Im_(seq_^\_k))_._n_)
let n be Element of NAT ; ::_thesis: ( ((Re seq) ^\ k) . n = (Re (seq ^\ k)) . n & ((Im seq) ^\ k) . n = (Im (seq ^\ k)) . n )
thus ((Re seq) ^\ k) . n = (Re seq) . (n + k) by NAT_1:def_3
.= Re (seq . (n + k)) by Def5
.= Re ((seq ^\ k) . n) by NAT_1:def_3
.= (Re (seq ^\ k)) . n by Def5 ; ::_thesis: ((Im seq) ^\ k) . n = (Im (seq ^\ k)) . n
thus ((Im seq) ^\ k) . n = (Im seq) . (n + k) by NAT_1:def_3
.= Im (seq . (n + k)) by Def6
.= Im ((seq ^\ k) . n) by NAT_1:def_3
.= (Im (seq ^\ k)) . n by Def6 ; ::_thesis: verum
end;
hence  ( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) ) by FUNCT_2:63; ::_thesis: verum
end;

definition
let s be Complex_Sequence;
:: original: Partial_Sums
redefine func Partial_Sums s ->  Complex_Sequence;
coherence
 Partial_Sums s is Complex_Sequence
proof
A1: dom (Partial_Sums s) = NAT by PARTFUN1:def_2;
 rng (Partial_Sums s) c= COMPLEX by VALUED_0:def_1;
then  Partial_Sums s is PartFunc of NAT,COMPLEX by A1, RELSET_1:4;
hence  Partial_Sums s is Complex_Sequence ; ::_thesis: verum
end;
end;

definition
let seq be Complex_Sequence;
func Sum seq ->  Element of COMPLEX  equals :: COMSEQ_3:def 7
 lim (Partial_Sums seq);
coherence
 lim (Partial_Sums seq) is Element of COMPLEX ;
end;

:: deftheorem  defines Sum COMSEQ_3:def_7_:_
 for seq being Complex_Sequence holds Sum seq = lim (Partial_Sums seq);

theorem Th24: :: COMSEQ_3:24
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
for m being Element of NAT holds (Partial_Sums seq) . m = 0c
proof
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies for m being Element of NAT holds (Partial_Sums seq) . m = 0c )
defpred S1[ Element of NAT ] means seq . $1 = (Partial_Sums seq) . $1;
assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: for m being Element of NAT holds (Partial_Sums seq) . m = 0c
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
thus seq . (k + 1) = 0c + (seq . (k + 1))
.= ((Partial_Sums seq) . k) + (seq . (k + 1)) by A1, A3
.= (Partial_Sums seq) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum
end;
let m be Element of NAT ; ::_thesis: (Partial_Sums seq) . m = 0c
A4: S1[ 0 ] by SERIES_1:def_1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
then  seq = Partial_Sums seq by FUNCT_2:63;
hence  (Partial_Sums seq) . m = 0c by A1; ::_thesis: verum
end;

theorem Th25: :: COMSEQ_3:25
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
for m being Element of NAT holds (Partial_Sums |.seq.|) . m = 0
proof
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies for m being Element of NAT holds (Partial_Sums |.seq.|) . m = 0 )
defpred S1[ Element of NAT ] means |.seq.| . $1 = (Partial_Sums |.seq.|) . $1;
assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: for m being Element of NAT holds (Partial_Sums |.seq.|) . m = 0
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
thus |.seq.| . (k + 1) = |.0c.| + (|.seq.| . (k + 1)) by COMPLEX1:44
.= |.(seq . k).| + (|.seq.| . (k + 1)) by A1
.= ((Partial_Sums |.seq.|) . k) + (|.seq.| . (k + 1)) by A3, VALUED_1:18
.= (Partial_Sums |.seq.|) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum
end;
let m be Element of NAT ; ::_thesis: (Partial_Sums |.seq.|) . m = 0
A4: S1[ 0 ] by SERIES_1:def_1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence (Partial_Sums |.seq.|) . m = |.seq.| . m
.= |.(seq . m).| by VALUED_1:18
.= 0 by A1, COMPLEX1:44 ;
::_thesis: verum
end;

theorem Th26: :: COMSEQ_3:26
for seq being Complex_Sequence holds
( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) )
proof
let seq be Complex_Sequence; ::_thesis: ( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) )
defpred S1[ Element of NAT ] means (Partial_Sums (Re seq)) . $1 = (Re (Partial_Sums seq)) . $1;
defpred S2[ Element of NAT ] means (Partial_Sums (Im seq)) . $1 = (Im (Partial_Sums seq)) . $1;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
then (Partial_Sums (Re seq)) . (k + 1) = ((Re (Partial_Sums seq)) . k) + ((Re seq) . (k + 1)) by SERIES_1:def_1
.= ((Re (Partial_Sums seq)) . k) + (Re (seq . (k + 1))) by Def5
.= (Re ((Partial_Sums seq) . k)) + (Re (seq . (k + 1))) by Def5
.= Re (((Partial_Sums seq) . k) + (seq . (k + 1))) by COMPLEX1:8
.= Re ((Partial_Sums seq) . (k + 1)) by SERIES_1:def_1
.= (Re (Partial_Sums seq)) . (k + 1) by Def5 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A2: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume  S2[k] ; ::_thesis: S2[k + 1]
then (Partial_Sums (Im seq)) . (k + 1) = ((Im (Partial_Sums seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def_1
.= ((Im (Partial_Sums seq)) . k) + (Im (seq . (k + 1))) by Def6
.= (Im ((Partial_Sums seq) . k)) + (Im (seq . (k + 1))) by Def6
.= Im (((Partial_Sums seq) . k) + (seq . (k + 1))) by COMPLEX1:8
.= Im ((Partial_Sums seq) . (k + 1)) by SERIES_1:def_1
.= (Im (Partial_Sums seq)) . (k + 1) by Def6 ;
hence  S2[k + 1] ; ::_thesis: verum
end;
(Partial_Sums (Im seq)) . 0 = (Im seq) . 0 by SERIES_1:def_1
.= Im (seq . 0) by Def6
.= Im ((Partial_Sums seq) . 0) by SERIES_1:def_1
.= (Im (Partial_Sums seq)) . 0 by Def6 ;
then A3: S2[ 0 ] ;
A4: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A3, A2);
(Partial_Sums (Re seq)) . 0 = (Re seq) . 0 by SERIES_1:def_1
.= Re (seq . 0) by Def5
.= Re ((Partial_Sums seq) . 0) by SERIES_1:def_1
.= (Re (Partial_Sums seq)) . 0 by Def5 ;
then A5: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1);
hence  ( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) ) by A4, FUNCT_2:63; ::_thesis: verum
end;

theorem Th27: :: COMSEQ_3:27
for seq1, seq2 being Complex_Sequence holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by SERIES_1:5;

theorem Th28: :: COMSEQ_3:28
for seq1, seq2 being Complex_Sequence holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
A1: Im ((Partial_Sums seq1) - (Partial_Sums seq2)) = (Im (Partial_Sums seq1)) - (Im (Partial_Sums seq2)) by Th18
.= (Partial_Sums (Im seq1)) - (Im (Partial_Sums seq2)) by Th26
.= (Partial_Sums (Im seq1)) - (Partial_Sums (Im seq2)) by Th26
.= Partial_Sums ((Im seq1) - (Im seq2)) by SERIES_1:6
.= Partial_Sums (Im (seq1 - seq2)) by Th18
.= Im (Partial_Sums (seq1 - seq2)) by Th26 ;
Re ((Partial_Sums seq1) - (Partial_Sums seq2)) = (Re (Partial_Sums seq1)) - (Re (Partial_Sums seq2)) by Th18
.= (Partial_Sums (Re seq1)) - (Re (Partial_Sums seq2)) by Th26
.= (Partial_Sums (Re seq1)) - (Partial_Sums (Re seq2)) by Th26
.= Partial_Sums ((Re seq1) - (Re seq2)) by SERIES_1:6
.= Partial_Sums (Re (seq1 - seq2)) by Th18
.= Re (Partial_Sums (seq1 - seq2)) by Th26 ;
hence  (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by A1, Th14; ::_thesis: verum
end;

theorem Th29: :: COMSEQ_3:29
for seq being Complex_Sequence
for z being complex number holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)
proof
let seq be Complex_Sequence; ::_thesis: for z being complex number holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)
let z be complex number ; ::_thesis: Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)
defpred S1[ Element of NAT ] means (Partial_Sums (z (#) seq)) . $1 = (z (#) (Partial_Sums seq)) . $1;
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(Partial_Sums (z (#) seq)) . (n + 1) = ((Partial_Sums (z (#) seq)) . n) + ((z (#) seq) . (n + 1)) by SERIES_1:def_1
.= (z * ((Partial_Sums seq) . n)) + ((z (#) seq) . (n + 1)) by A2, VALUED_1:6
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by VALUED_1:6
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1)))
.= z * ((Partial_Sums seq) . (n + 1)) by SERIES_1:def_1
.= (z (#) (Partial_Sums seq)) . (n + 1) by VALUED_1:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums (z (#) seq)) . 0 = (z (#) seq) . 0 by SERIES_1:def_1
.= z * (seq . 0) by VALUED_1:6
.= z * ((Partial_Sums seq) . 0) by SERIES_1:def_1
.= (z (#) (Partial_Sums seq)) . 0 by VALUED_1:6 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_3:30
for seq being Complex_Sequence
for k being Element of NAT holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
proof
let seq be Complex_Sequence; ::_thesis: for k being Element of NAT holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
let k be Element of NAT ; ::_thesis: |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
defpred S1[ Element of NAT ] means |.((Partial_Sums seq) . $1).| <= (Partial_Sums |.seq.|) . $1;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
then A2: |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by XREAL_1:6;
 ( |.((Partial_Sums seq) . (k + 1)).| = |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| & |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| <= |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| ) by COMPLEX1:56, SERIES_1:def_1;
then  |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by A2, XXREAL_0:2;
then  |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + (|.seq.| . (k + 1)) by VALUED_1:18;
hence  S1[k + 1] by SERIES_1:def_1; ::_thesis: verum
end;
(Partial_Sums |.seq.|) . 0 = |.seq.| . 0 by SERIES_1:def_1
.= |.(seq . 0).| by VALUED_1:18 ;
then A3: S1[ 0 ] by SERIES_1:def_1;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1);
hence  |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k ; ::_thesis: verum
end;

theorem Th31: :: COMSEQ_3:31
for seq being Complex_Sequence
for m, n being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
proof
let seq be Complex_Sequence; ::_thesis: for m, n being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
let m, n be Element of NAT ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
A1: for n, k being Element of NAT holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
proof
let n be Element of NAT ; ::_thesis: for k being Element of NAT holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
defpred S1[ Element of NAT ] means  0 <= ((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n);
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A3: ((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n) = (((Partial_Sums |.seq.|) . (n + k)) + (|.seq.| . ((n + k) + 1))) - ((Partial_Sums |.seq.|) . n) by SERIES_1:def_1
.= (((Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - ((Partial_Sums |.seq.|) . n) by VALUED_1:18
.= (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).| ;
A4: 0 <= |.(seq . ((n + k) + 1)).| by COMPLEX1:46;
assume  S1[k] ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A3, A4; ::_thesis: verum
end;
A5: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); ::_thesis: verum
end;
A6: for n, k being Element of NAT holds abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
proof
let n, k be Element of NAT ; ::_thesis: abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) by A1;
hence  abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) by ABSVALUE:def_1; ::_thesis: verum
end;
A7: for n, m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) )
assume  n <= m ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
then consider k being Nat such that
A8: m = n + k by NAT_1:10;
A9: for k being Element of NAT holds |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))
proof
defpred S1[ Element of NAT ] means |.(((Partial_Sums seq) . (n + $1)) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n));
A10: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
then A11: ( |.((((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| <= |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).| & |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).| <= (abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))) + |.(seq . ((n + k) + 1)).| ) by COMPLEX1:56, XREAL_1:6;
A12: |.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).| = |.((((Partial_Sums seq) . (n + k)) + (seq . ((n + k) + 1))) - ((Partial_Sums seq) . n)).| by SERIES_1:def_1
.= |.((((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| ;
(abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))) + |.(seq . ((n + k) + 1)).| = (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).| by A6
.= (((Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - ((Partial_Sums |.seq.|) . n)
.= (((Partial_Sums |.seq.|) . (n + k)) + (|.seq.| . ((n + k) + 1))) - ((Partial_Sums |.seq.|) . n) by VALUED_1:18
.= ((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n) by SERIES_1:def_1
.= abs (((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n)) by A6 ;
hence  S1[k + 1] by A12, A11, XXREAL_0:2; ::_thesis: verum
end;
A13: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A10); ::_thesis: verum
end;
 k in NAT by ORDINAL1:def_12;
hence  |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A9, A8; ::_thesis: verum
end;
 for n, m being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
proof
let n, m be Element of NAT ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
 ( m <= n implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) )
proof
assume  m <= n ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
then A14: |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= abs (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)) by A7;
abs (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)) = abs (- (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m))) by COMPLEX1:52
.= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ;
hence  |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A14, COMPLEX1:60; ::_thesis: verum
end;
hence  |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A7; ::_thesis: verum
end;
hence  |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ; ::_thesis: verum
end;

theorem Th32: :: COMSEQ_3:32
for seq being Complex_Sequence
for k being Element of NAT holds
( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )
proof
let seq be Complex_Sequence; ::_thesis: for k being Element of NAT holds
( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )
let k be Element of NAT ; ::_thesis: ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_((Partial_Sums_(Re_seq))_^\_k)_._n_=_(Re_((Partial_Sums_seq)_^\_k))_._n_&_((Partial_Sums_(Im_seq))_^\_k)_._n_=_(Im_((Partial_Sums_seq)_^\_k))_._n_)
let n be Element of NAT ; ::_thesis: ( ((Partial_Sums (Re seq)) ^\ k) . n = (Re ((Partial_Sums seq) ^\ k)) . n & ((Partial_Sums (Im seq)) ^\ k) . n = (Im ((Partial_Sums seq) ^\ k)) . n )
thus ((Partial_Sums (Re seq)) ^\ k) . n = (Partial_Sums (Re seq)) . (n + k) by NAT_1:def_3
.= (Re (Partial_Sums seq)) . (n + k) by Th26
.= Re ((Partial_Sums seq) . (n + k)) by Def5
.= Re (((Partial_Sums seq) ^\ k) . n) by NAT_1:def_3
.= (Re ((Partial_Sums seq) ^\ k)) . n by Def5 ; ::_thesis: ((Partial_Sums (Im seq)) ^\ k) . n = (Im ((Partial_Sums seq) ^\ k)) . n
thus ((Partial_Sums (Im seq)) ^\ k) . n = (Partial_Sums (Im seq)) . (n + k) by NAT_1:def_3
.= (Im (Partial_Sums seq)) . (n + k) by Th26
.= Im ((Partial_Sums seq) . (n + k)) by Def6
.= Im (((Partial_Sums seq) ^\ k) . n) by NAT_1:def_3
.= (Im ((Partial_Sums seq) ^\ k)) . n by Def6 ; ::_thesis: verum
end;
hence  ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) ) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_3:33
for seq1, seq being Complex_Sequence st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
proof
let seq1, seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 )
assume A1: for n being Element of NAT holds seq1 . n = seq . 0 ; ::_thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(Re_seq1)_._n_=_(Re_seq)_._0_&_(Im_seq1)_._n_=_(Im_seq)_._0_)
let n be Element of NAT ; ::_thesis: ( (Re seq1) . n = (Re seq) . 0 & (Im seq1) . n = (Im seq) . 0 )
thus (Re seq1) . n = Re (seq1 . n) by Def5
.= Re (seq . 0) by A1
.= (Re seq) . 0 by Def5 ; ::_thesis: (Im seq1) . n = (Im seq) . 0
thus (Im seq1) . n = Im (seq1 . n) by Def6
.= Im (seq . 0) by A1
.= (Im seq) . 0 by Def6 ; ::_thesis: verum
end;
A3: Im (Partial_Sums (seq ^\ 1)) = Partial_Sums (Im (seq ^\ 1)) by Th26
.= Partial_Sums ((Im seq) ^\ 1) by Th23
.= ((Partial_Sums (Im seq)) ^\ 1) - (Im seq1) by A2, SERIES_1:11
.= (Im ((Partial_Sums seq) ^\ 1)) - (Im seq1) by Th32
.= Im (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ;
Re (Partial_Sums (seq ^\ 1)) = Partial_Sums (Re (seq ^\ 1)) by Th26
.= Partial_Sums ((Re seq) ^\ 1) by Th23
.= ((Partial_Sums (Re seq)) ^\ 1) - (Re seq1) by A2, SERIES_1:11
.= (Re ((Partial_Sums seq) ^\ 1)) - (Re seq1) by Th32
.= Re (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ;
hence  Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A3, Th14; ::_thesis: verum
end;

theorem Th34: :: COMSEQ_3:34
for seq being Complex_Sequence holds Partial_Sums |.seq.| is non-decreasing
proof
let seq be Complex_Sequence; ::_thesis: Partial_Sums |.seq.| is non-decreasing
 for n being Element of NAT holds 0 <= |.seq.| . n by Lm3;
hence  Partial_Sums |.seq.| is non-decreasing by SERIES_1:16; ::_thesis: verum
end;

registration
let seq be Complex_Sequence;
cluster Partial_Sums |.seq.| ->  non-decreasing for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Partial_Sums |.seq.| holds
b1 is non-decreasing by Th34;
end;

theorem :: COMSEQ_3:35
for seq1, seq2 being Complex_Sequence
for m being Element of NAT st ( for n being Element of NAT st n <= m holds
seq1 . n = seq2 . n ) holds
(Partial_Sums seq1) . m = (Partial_Sums seq2) . m
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: for m being Element of NAT st ( for n being Element of NAT st n <= m holds
seq1 . n = seq2 . n ) holds
(Partial_Sums seq1) . m = (Partial_Sums seq2) . m
let m be Element of NAT ; ::_thesis: ( ( for n being Element of NAT st n <= m holds
seq1 . n = seq2 . n ) implies (Partial_Sums seq1) . m = (Partial_Sums seq2) . m )
defpred S1[ Element of NAT ] means ( $1 <= m implies (Partial_Sums seq1) . $1 = (Partial_Sums seq2) . $1 );
assume A1: for n being Element of NAT st n <= m holds
seq1 . n = seq2 . n ; ::_thesis: (Partial_Sums seq1) . m = (Partial_Sums seq2) . m
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
assume A4: k + 1 <= m ; ::_thesis: (Partial_Sums seq1) . (k + 1) = (Partial_Sums seq2) . (k + 1)
 k < k + 1 by XREAL_1:29;
hence (Partial_Sums seq1) . (k + 1) = ((Partial_Sums seq2) . k) + (seq1 . (k + 1)) by A3, A4, SERIES_1:def_1, XXREAL_0:2
.= ((Partial_Sums seq2) . k) + (seq2 . (k + 1)) by A1, A4
.= (Partial_Sums seq2) . (k + 1) by SERIES_1:def_1 ;
::_thesis: verum
end;
A5: S1[ 0 ]
proof
assume  0 <= m ; ::_thesis: (Partial_Sums seq1) . 0 = (Partial_Sums seq2) . 0
thus (Partial_Sums seq1) . 0 = seq1 . 0 by SERIES_1:def_1
.= seq2 . 0 by A1
.= (Partial_Sums seq2) . 0 by SERIES_1:def_1 ; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2);
hence  (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ; ::_thesis: verum
end;

theorem Th36: :: COMSEQ_3:36
for z being Element of COMPLEX st 1r <> z holds
for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z)
proof
let z be Element of COMPLEX ; ::_thesis: ( 1r <> z implies for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z) )
now__::_thesis:_for_z_being_Element_of_COMPLEX_st_1r_<>_z_holds_
for_n_being_Element_of_NAT_holds_S1[n]
let z be Element of COMPLEX ; ::_thesis: ( 1r <> z implies for n being Element of NAT holds S1[n] )
defpred S1[ Element of NAT ] means (Partial_Sums (z GeoSeq)) . $1 = (1r - (z #N ($1 + 1))) / (1r - z);
assume  1r <> z ; ::_thesis: for n being Element of NAT holds S1[n]
then A1: 1r - z <> 0c ;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
hence (Partial_Sums (z GeoSeq)) . (n + 1) = ((1r - (z #N (n + 1))) / (1r - z)) + ((z #N (n + 1)) * 1r) by COMPLEX1:def_4, SERIES_1:def_1
.= ((1r - (z #N (n + 1))) / (1r - z)) + ((z #N (n + 1)) * ((1r - z) / (1r - z))) by A1, COMPLEX1:def_4, XCMPLX_1:60
.= ((1r - (z #N (n + 1))) / (1r - z)) + (((z #N (n + 1)) * (1r - z)) / (1r - z)) by XCMPLX_1:74
.= ((1r - (z #N (n + 1))) + ((z #N (n + 1)) - ((z #N (n + 1)) * z))) / (1r - z) by COMPLEX1:def_4, XCMPLX_1:62
.= (1r - ((z #N (n + 1)) * z)) / (1r - z)
.= (1r - (z #N ((n + 1) + 1))) / (1r - z) by NEWTON:6 ;
::_thesis: verum
end;
(Partial_Sums (z GeoSeq)) . 0 = (z GeoSeq) . 0 by SERIES_1:def_1
.= 1r by Def1
.= (1r - (1 * z)) / (1r - z) by A1, COMPLEX1:def_4, XCMPLX_1:60
.= (1r - (z #N (0 + 1))) / (1r - z) by NEWTON:5 ;
then A3: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); ::_thesis: verum
end;
hence  ( 1r <> z implies for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z) ) ; ::_thesis: verum
end;

theorem Th37: :: COMSEQ_3:37
for seq being Complex_Sequence
for z being Element of COMPLEX st z <> 1r & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds
for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z))
proof
let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st z <> 1r & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds
for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z))
let z be Element of COMPLEX ; ::_thesis: ( z <> 1r & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) implies for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) )
assume that
A1: z <> 1r and
A2: for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z))
defpred S1[ Element of NAT ] means seq . $1 = (seq . 0) * ((z GeoSeq) . $1);
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then seq . (n + 1) = z * ((seq . 0) * ((z GeoSeq) . n)) by A2
.= (seq . 0) * (z * ((z GeoSeq) . n))
.= (seq . 0) * ((z GeoSeq) . (n + 1)) by Def1 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z))
seq . 0 = (seq . 0) * 1r by COMPLEX1:def_4
.= (seq . 0) * ((z GeoSeq) . 0) by Def1 ;
then A4: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
then  Partial_Sums seq = Partial_Sums ((seq . 0) (#) (z GeoSeq)) by VALUED_1:7
.= (seq . 0) (#) (Partial_Sums (z GeoSeq)) by Th29 ;
hence (Partial_Sums seq) . n = (seq . 0) * ((Partial_Sums (z GeoSeq)) . n) by VALUED_1:6
.= (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) by A1, Th36 ;
::_thesis: verum
end;

begin

theorem Th38: :: COMSEQ_3:38
for a, b being Real_Sequence
for c being 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 ) iff c is convergent )
proof
let a, b be 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
( ( a is convergent & b is convergent ) iff c is convergent )
let c be 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 ) iff c is convergent ) )
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 ) 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 number  such that
A4: 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) - a1) < p by A2, SEQ_2:def_6;
consider b1 being real number  such that
A5: 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) - b1) < p by A3, SEQ_2:def_6;
reconsider a1 = a1, b1 = b1 as Real by XREAL_0:def_1;
reconsider g = a1 + (b1 * <i>) as Element of COMPLEX by XCMPLX_0:def_2;
take  g ; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.((c . b3) - g).| ) )
 for p being 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 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 A6: 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 consider n1 being Element of NAT  such that
A7: for m being Element of NAT st n1 <= m holds
abs ((a . m) - a1) < p / 2 by A4;
consider n2 being Element of NAT  such that
A8: for m being Element of NAT st n2 <= m holds
abs ((b . m) - b1) < p / 2 by A5, A6;
 ( n1 <= n1 + n2 & n2 <= n1 + n2 ) by NAT_1:11;
then consider n being Element of NAT  such that
A9: n1 <= n and
A10: n2 <= n ;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p
 for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p
proof
let m be Element of 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: abs ((b . m) - b1) < p / 2 by A8;
 n1 <= m by A9, A13, XXREAL_0:2;
then  abs ((a . m) - a1) < p / 2 by A7;
then A15: (abs ((a . m) - a1)) + (abs ((b . m) - b1)) < (p / 2) + (p / 2) by A14, XREAL_1:8;
 |.((c . m) - g).| <= (abs (Re ((c . m) - g))) + (abs (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 Element of NAT st n <= m holds
|.((c . m) - g).| < p ; ::_thesis: verum
end;
hence  for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.((c . b3) - g).| ) ) ; ::_thesis: verum
end;
assume  c is convergent ; ::_thesis: ( a is convergent & b is convergent )
then consider z being Element of COMPLEX  such that
A16: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((c . m) - z).| < p by COMSEQ_2:def_5;
thus  a is convergent ::_thesis: b is convergent
proof
reconsider z = z as Element of COMPLEX ;
take  Re z ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((a . b3) - (Re z)) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((a . b2) - (Re z)) ) )
assume A17: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((a . b2) - (Re z)) )
 p is Real by XREAL_0:def_1;
then consider n being Element of NAT  such that
A18: for m being Element of NAT st n <= m holds
|.((c . m) - z).| < p by A16, A17;
take  n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= abs ((a . b1) - (Re z)) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((a . m) - (Re z)) )
assume  n <= m ; ::_thesis: not p <= abs ((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  abs ((a . m) - (Re z)) <= |.((c . m) - z).| by Th13;
hence  not p <= abs ((a . m) - (Re z)) by A19, XXREAL_0:2; ::_thesis: verum
end;
take  Im z ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((b . b3) - (Im z)) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((b . b2) - (Im z)) ) )
assume A20: p > 0 ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((b . b2) - (Im z)) )
 p is Real by XREAL_0:def_1;
then consider n being Element of NAT  such that
A21: for m being Element of NAT st n <= m holds
|.((c . m) - z).| < p by A16, A20;
take  n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= abs ((b . b1) - (Im z)) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((b . m) - (Im z)) )
assume  n <= m ; ::_thesis: not p <= abs ((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  abs ((b . m) - (Im z)) <= |.((c . m) - z).| by A23, Th13;
hence  not p <= abs ((b . m) - (Im z)) by A22, XXREAL_0:2; ::_thesis: verum
end;

theorem Th39: :: COMSEQ_3:39
for a, b being convergent Real_Sequence
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>) )
proof
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>) ) )
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: ( 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>)
 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 A3: 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 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: 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 A8: n <= m ; ::_thesis: |.((c . m) - g).| < p
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: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).| <= (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: verum
end;
hence  lim c = (lim a) + ((lim b) * <i>) by A2, COMSEQ_2:def_6; ::_thesis: verum
end;

theorem Th40: :: COMSEQ_3:40
for a, b being Real_Sequence
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) )
proof
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) )
A2: 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 )
assume A3: 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
 p is Real by XREAL_0:def_1;
then consider n being Element of NAT  such that
A4: for m being Element of NAT st n <= m holds
|.((c . m) - (lim c)).| < p by A3, COMSEQ_2:def_6;
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 A5: |.((c . m) - (lim c)).| < p by A4;
 ( Im (c . m) = b . m & Im ((c . m) - (lim c)) = (Im (c . m)) - (Im (lim c)) ) by A1, COMPLEX1:19;
then  abs ((b . m) - (Im (lim c))) <= |.((c . m) - (lim c)).| by Th13;
hence  abs ((b . m) - (Im (lim c))) < p by A5, XXREAL_0:2; ::_thesis: verum
end;
A6: 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 )
assume A7: 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
 p is Real by XREAL_0:def_1;
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_6;
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 )
 Re (c . m) = a . m by A1;
then  Re ((c . m) - (lim c)) = (a . m) - (Re (lim c)) by COMPLEX1:19;
then A9: abs ((a . m) - (Re (lim c))) <= |.((c . m) - (lim c)).| by Th13;
assume  n <= m ; ::_thesis: abs ((a . m) - (Re (lim c))) < p
then  |.((c . m) - (lim c)).| < p by A8;
hence  abs ((a . m) - (Re (lim c))) < p by A9, XXREAL_0:2; ::_thesis: verum
end;
 ( a is convergent & b is convergent ) by A1, Th38;
hence  ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) by A6, A2, SEQ_2:def_7; ::_thesis: verum
end;

theorem Th41: :: COMSEQ_3:41
for c being convergent Complex_Sequence holds
( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) )
proof
let c be convergent Complex_Sequence; ::_thesis: ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) )
 ( ( for n being Element of NAT holds (Re c) . n = Re (c . n) ) & ( for n being Element of NAT holds (Im c) . n = Im (c . n) ) ) by Def5, Def6;
hence  ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) ) by Th40; ::_thesis: verum
end;

registration
let c be convergent Complex_Sequence;
cluster Re c ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Re c holds
b1 is convergent by Th41;
cluster Im c ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Im c holds
b1 is convergent by Th41;
end;

theorem Th42: :: COMSEQ_3:42
for c being Complex_Sequence st Re c is convergent & Im c is convergent holds
( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) )
proof
let c be Complex_Sequence; ::_thesis: ( Re c is convergent & Im c is convergent implies ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) )
assume A1: ( Re c is convergent & Im c is convergent ) ; ::_thesis: ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) )
A2: ( ( for n being Element of NAT holds (Re c) . n = Re (c . n) ) & ( for n being Element of NAT holds (Im c) . n = Im (c . n) ) ) by Def5, Def6;
then  lim c = (lim (Re c)) + ((lim (Im c)) * <i>) by A1, Th39;
hence  ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) by A1, A2, Th39, COMPLEX1:12; ::_thesis: verum
end;

theorem Th43: :: COMSEQ_3:43
for seq being Complex_Sequence
for z being Element of COMPLEX st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) holds
( seq is convergent & lim seq = 0c )
proof
let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) holds
( seq is convergent & lim seq = 0c )
let z be Element of COMPLEX ; ::_thesis: ( 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) implies ( seq is convergent & lim seq = 0c ) )
assume that
A1: 0 < |.z.| and
A2: |.z.| < 1 ; ::_thesis: ( not seq . 0 = z or ex n being Element of NAT st not seq . (n + 1) = (seq . n) * z or ( seq is convergent & lim seq = 0c ) )
deffunc H1( Element of NAT ) ->  Element of REAL = |.z.| to_power ($1 + 1);
consider rseq1 being Real_Sequence such that
A3: for n being Element of NAT holds rseq1 . n = H1(n) from SEQ_1:sch_1();
assume that
A4: seq . 0 = z and
A5: for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ; ::_thesis: ( seq is convergent & lim seq = 0c )
A6: for n being Element of NAT holds |.(seq . n).| = |.z.| to_power (n + 1)
proof
defpred S1[ Element of NAT ] means |.(seq . $1).| = |.z.| to_power ($1 + 1);
A7: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; ::_thesis: S1[k + 1]
|.(seq . (k + 1)).| = |.((seq . k) * z).| by A5
.= (|.z.| to_power (k + 1)) * |.z.| by A8, COMPLEX1:65
.= (|.z.| to_power (k + 1)) * (|.z.| to_power 1) by POWER:25
.= |.z.| to_power ((k + 1) + 1) by A1, POWER:27 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A9: S1[ 0 ] by A4, POWER:25;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7);
hence  for n being Element of NAT holds |.(seq . n).| = |.z.| to_power (n + 1) ; ::_thesis: verum
end;
A10: now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Re_seq))_._n_<=_rseq1_._n
let n be Element of NAT ; ::_thesis: (abs (Re seq)) . n <= rseq1 . n
 (abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:12;
then A11: (abs (Re seq)) . n = abs (Re (seq . n)) by Def5;
 ( abs (Re (seq . n)) <= |.(seq . n).| & |.(seq . n).| = |.z.| to_power (n + 1) ) by A6, Th13;
hence  (abs (Re seq)) . n <= rseq1 . n by A3, A11; ::_thesis: verum
end;
A12: now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Im_seq))_._n_<=_rseq1_._n
let n be Element of NAT ; ::_thesis: (abs (Im seq)) . n <= rseq1 . n
A13: |.(seq . n).| = |.z.| to_power (n + 1) by A6;
 ( (abs (Im seq)) . n = abs ((Im seq) . n) & abs (Im (seq . n)) <= |.(seq . n).| ) by Th13, SEQ_1:12;
then  (abs (Im seq)) . n <= |.z.| to_power (n + 1) by A13, Def6;
hence  (abs (Im seq)) . n <= rseq1 . n by A3; ::_thesis: verum
end;
 C . 0 = 0 by FUNCOP_1:7;
then A14: lim C = 0 by SEQ_4:25;
A15: ( rseq1 is convergent & lim rseq1 = 0 ) by A1, A2, A3, SERIES_1:1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Re_seq))_._n
let n be Element of NAT ; ::_thesis: C . n <= (abs (Re seq)) . n
 (abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:12;
then  0 <= (abs (Re seq)) . n by COMPLEX1:46;
hence  C . n <= (abs (Re seq)) . n by FUNCOP_1:7; ::_thesis: verum
end;
then A16: ( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 ) by A14, A15, A10, SEQ_2:19, SEQ_2:20;
then A17: Re seq is convergent by SEQ_4:15;
now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Im_seq))_._n
let n be Element of NAT ; ::_thesis: C . n <= (abs (Im seq)) . n
 (abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:12;
then  0 <= (abs (Im seq)) . n by COMPLEX1:46;
hence  C . n <= (abs (Im seq)) . n by FUNCOP_1:7; ::_thesis: verum
end;
then A18: ( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 ) by A14, A15, A12, SEQ_2:19, SEQ_2:20;
then A19: Im seq is convergent by SEQ_4:15;
 lim (Im seq) = 0 by A18, SEQ_4:15;
then A20: Im (lim seq) = 0 by A17, A19, Th42;
 lim (Re seq) = 0 by A16, SEQ_4:15;
then  Re (lim seq) = 0 by A17, A19, Th42;
hence  ( seq is convergent & lim seq = 0c ) by A17, A19, A20, Lm1, Th42, COMPLEX1:13; ::_thesis: verum
end;

theorem Th44: :: COMSEQ_3:44
for seq being Complex_Sequence
for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) holds
( seq is convergent & lim seq = 0c )
proof
let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) holds
( seq is convergent & lim seq = 0c )
let z be Element of COMPLEX ; ::_thesis: ( |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) implies ( seq is convergent & lim seq = 0c ) )
assume that
A1: |.z.| < 1 and
A2: for n being Element of NAT holds seq . n = z #N (n + 1) ; ::_thesis: ( seq is convergent & lim seq = 0c )
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._(n_+_1)_=_(seq_._n)_*_z
let n be Element of NAT ; ::_thesis: seq . (n + 1) = (seq . n) * z
thus seq . (n + 1) = z #N ((n + 1) + 1) by A2
.= (z #N (n + 1)) * z by NEWTON:6
.= (seq . n) * z by A2 ; ::_thesis: verum
end;
A4: now__::_thesis:_(_|.z.|_=_0_implies_(_seq_is_convergent_&_seq_is_convergent_&_lim_seq_=_0c_)_)
assume  |.z.| = 0 ; ::_thesis: ( seq is convergent & seq is convergent & lim seq = 0c )
then A5: z = 0c by COMPLEX1:45;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_=_0c
let n be Element of NAT ; ::_thesis: seq . n = 0c
thus seq . n = 0c #N (n + 1) by A2, A5
.= ((0c GeoSeq) . n) * 0c by Def1
.= 0c ; ::_thesis: verum
end;
hence  seq is convergent by COMSEQ_2:9; ::_thesis: ( seq is convergent & lim seq = 0c )
thus  ( seq is convergent & lim seq = 0c ) by A6, COMSEQ_2:9, COMSEQ_2:10; ::_thesis: verum
end;
A7: seq . 0 = z #N (0 + 1) by A2
.= z by NEWTON:5 ;
now__::_thesis:_(_|.z.|_<>_0_implies_(_seq_is_convergent_&_lim_seq_=_0c_)_)
A8: 0 <= |.z.| by COMPLEX1:46;
assume  |.z.| <> 0 ; ::_thesis: ( seq is convergent & lim seq = 0c )
hence  ( seq is convergent & lim seq = 0c ) by A1, A7, A3, A8, Th43; ::_thesis: verum
end;
hence  ( seq is convergent & lim seq = 0c ) by A4; ::_thesis: verum
end;

theorem :: COMSEQ_3:45
for seq being Complex_Sequence
for r being Real st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.(seq . n).| >= r & |.seq.| is convergent holds
lim |.seq.| <> 0
proof
let seq be Complex_Sequence; ::_thesis: for r being Real st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.(seq . n).| >= r & |.seq.| is convergent holds
lim |.seq.| <> 0
let r be Real; ::_thesis: ( r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.(seq . n).| >= r & |.seq.| is convergent implies lim |.seq.| <> 0 )
assume that
A1: r > 0 and
A2: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.(seq . n).| >= r ; ::_thesis: ( not |.seq.| is convergent or lim |.seq.| <> 0 )
consider m being Element of NAT  such that
A3: for n being Element of NAT st n >= m holds
|.(seq . n).| >= r by A2;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
abs_(|.seq.|_._n)_>=_r
let n be Element of NAT ; ::_thesis: ( n >= m implies abs (|.seq.| . n) >= r )
assume A4: n >= m ; ::_thesis: abs (|.seq.| . n) >= r
 0 <= |.seq.| . n by Lm3;
then  abs (|.seq.| . n) = |.seq.| . n by ABSVALUE:def_1
.= |.(seq . n).| by VALUED_1:18 ;
hence  abs (|.seq.| . n) >= r by A3, A4; ::_thesis: verum
end;
hence  ( not |.seq.| is convergent or lim |.seq.| <> 0 ) by A1, SERIES_1:38; ::_thesis: verum
end;

theorem Th46: :: COMSEQ_3:46
for seq being Complex_Sequence holds
( seq is convergent iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is convergent iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p )
A1: now__::_thesis:_(_(_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq_._m)_-_(seq_._n)).|_<_p_)_implies_(_Re_seq_is_convergent_&_Im_seq_is_convergent_&_seq_is_convergent_)_)
assume A2: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p ; ::_thesis: ( Re seq is convergent & Im seq is convergent & seq is convergent )
 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 (((Re seq) . m) - ((Re seq) . n)) < 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 (((Re seq) . m) - ((Re seq) . n)) < p )
assume A3: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Re seq) . m) - ((Re seq) . n)) < p
 p is Real by XREAL_0:def_1;
then consider n being Element of NAT  such that
A4: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p by A2, A3;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs (((Re seq) . m) - ((Re seq) . n)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Re seq) . m) - ((Re seq) . n)) < p )
assume  n <= m ; ::_thesis: abs (((Re seq) . m) - ((Re seq) . n)) < p
then A5: |.((seq . m) - (seq . n)).| < p by A4;
Re ((seq . m) - (seq . n)) = (Re (seq . m)) - (Re (seq . n)) by COMPLEX1:19
.= ((Re seq) . m) - (Re (seq . n)) by Def5
.= ((Re seq) . m) - ((Re seq) . n) by Def5 ;
then  abs (((Re seq) . m) - ((Re seq) . n)) <= |.((seq . m) - (seq . n)).| by Th13;
hence  abs (((Re seq) . m) - ((Re seq) . n)) < p by A5, XXREAL_0:2; ::_thesis: verum
end;
hence A6: Re seq is convergent by SEQ_4:41; ::_thesis: ( Im seq is convergent & seq is convergent )
 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 (((Im seq) . m) - ((Im seq) . n)) < 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 (((Im seq) . m) - ((Im seq) . n)) < p )
assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Im seq) . m) - ((Im seq) . n)) < p
 p is Real by XREAL_0:def_1;
then consider n being Element of NAT  such that
A8: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p by A2, A7;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs (((Im seq) . m) - ((Im seq) . n)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Im seq) . m) - ((Im seq) . n)) < p )
assume  n <= m ; ::_thesis: abs (((Im seq) . m) - ((Im seq) . n)) < p
then A9: |.((seq . m) - (seq . n)).| < p by A8;
Im ((seq . m) - (seq . n)) = (Im (seq . m)) - (Im (seq . n)) by COMPLEX1:19
.= ((Im seq) . m) - (Im (seq . n)) by Def6
.= ((Im seq) . m) - ((Im seq) . n) by Def6 ;
then  abs (((Im seq) . m) - ((Im seq) . n)) <= |.((seq . m) - (seq . n)).| by Th13;
hence  abs (((Im seq) . m) - ((Im seq) . n)) < p by A9, XXREAL_0:2; ::_thesis: verum
end;
hence  Im seq is convergent by SEQ_4:41; ::_thesis: seq is convergent
hence  seq is convergent by A6, Th42; ::_thesis: verum
end;
now__::_thesis:_(_seq_is_convergent_implies_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq_._m)_-_(seq_._n)).|_<_p_)
assume  seq is convergent ; ::_thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p
then consider z being Element of COMPLEX  such that
A10: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - z).| < p by COMSEQ_2:def_5;
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p
then consider n being Element of NAT  such that
A11: for m being Element of NAT st n <= m holds
|.((seq . m) - z).| < p / 2 by A10;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq . m) - (seq . n)).| < p )
assume  n <= m ; ::_thesis: |.((seq . m) - (seq . n)).| < p
then A12: |.((seq . m) - z).| < p / 2 by A11;
 |.((seq . n) - z).| < p / 2 by A11;
then  |.((seq . m) - z).| + |.((seq . n) - z).| < (p / 2) + (p / 2) by A12, XREAL_1:8;
then A13: |.((seq . m) - z).| + |.(z - (seq . n)).| < p by COMPLEX1:60;
 |.((seq . m) - (seq . n)).| <= |.((seq . m) - z).| + |.(z - (seq . n)).| by COMPLEX1:63;
hence  |.((seq . m) - (seq . n)).| < p by A13, XXREAL_0:2; ::_thesis: verum
end;
hence  ( seq is convergent iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p ) by A1; ::_thesis: verum
end;

theorem :: COMSEQ_3:47
for seq being Complex_Sequence st seq is convergent holds
for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
proof
let seq be Complex_Sequence; ::_thesis: ( seq is convergent implies for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p )
assume A1: seq is convergent ; ::_thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
then consider n being Element of NAT  such that
A2: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p / 2 by A1, Th46;
take  n ; ::_thesis: for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
now__::_thesis:_for_m,_l_being_Element_of_NAT_st_n_<=_m_&_n_<=_l_holds_
|.((seq_._m)_-_(seq_._l)).|_<_p
let m, l be Element of NAT ; ::_thesis: ( n <= m & n <= l implies |.((seq . m) - (seq . l)).| < p )
assume  ( n <= m & n <= l ) ; ::_thesis: |.((seq . m) - (seq . l)).| < p
then  ( |.((seq . m) - (seq . n)).| < p / 2 & |.((seq . l) - (seq . n)).| < p / 2 ) by A2;
then A3: |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).| < (p / 2) + (p / 2) by XREAL_1:8;
 |.(((seq . m) - (seq . n)) - ((seq . l) - (seq . n))).| <= |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).| by COMPLEX1:57;
hence  |.((seq . m) - (seq . l)).| < p by A3, XXREAL_0:2; ::_thesis: verum
end;
hence  for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p ; ::_thesis: verum
end;

theorem :: COMSEQ_3:48
for rseq being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0c )
proof
let rseq be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0c )
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0c ) )
assume that
A1: for n being Element of NAT holds |.(seq . n).| <= rseq . n and
A2: ( rseq is convergent & lim rseq = 0 ) ; ::_thesis: ( seq is convergent & lim seq = 0c )
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Re_seq))_._n
let n be Element of NAT ; ::_thesis: C . n <= (abs (Re seq)) . n
 (abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:12;
then  0 <= (abs (Re seq)) . n by COMPLEX1:46;
hence  C . n <= (abs (Re seq)) . n by FUNCOP_1:7; ::_thesis: verum
end;
 C . 0 = 0 by FUNCOP_1:7;
then A4: lim C = 0 by SEQ_4:25;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Re_seq))_._n_<=_rseq_._n
let n be Element of NAT ; ::_thesis: (abs (Re seq)) . n <= rseq . n
 (Re seq) . n = Re (seq . n) by Def5;
then A5: (abs (Re seq)) . n = abs (Re (seq . n)) by SEQ_1:12;
 ( abs (Re (seq . n)) <= |.(seq . n).| & |.(seq . n).| <= rseq . n ) by A1, Th13;
hence  (abs (Re seq)) . n <= rseq . n by A5, XXREAL_0:2; ::_thesis: verum
end;
then A6: ( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 ) by A2, A4, A3, SEQ_2:19, SEQ_2:20;
then A7: Re seq is convergent by SEQ_4:15;
A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Im_seq))_._n
let n be Element of NAT ; ::_thesis: C . n <= (abs (Im seq)) . n
 (abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:12;
then  0 <= (abs (Im seq)) . n by COMPLEX1:46;
hence  C . n <= (abs (Im seq)) . n by FUNCOP_1:7; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Im_seq))_._n_<=_rseq_._n
let n be Element of NAT ; ::_thesis: (abs (Im seq)) . n <= rseq . n
A9: ( (Im seq) . n = Im (seq . n) & (abs (Im seq)) . n = abs ((Im seq) . n) ) by Def6, SEQ_1:12;
 ( abs (Im (seq . n)) <= |.(seq . n).| & |.(seq . n).| <= rseq . n ) by A1, Th13;
hence  (abs (Im seq)) . n <= rseq . n by A9, XXREAL_0:2; ::_thesis: verum
end;
then A10: ( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 ) by A2, A4, A8, SEQ_2:19, SEQ_2:20;
then A11: Im seq is convergent by SEQ_4:15;
 lim (Im seq) = 0 by A10, SEQ_4:15;
then A12: Im (lim seq) = 0 by A7, A11, Th42;
 lim (Re seq) = 0 by A6, SEQ_4:15;
then  Re (lim seq) = 0 by A7, A11, Th42;
hence  ( seq is convergent & lim seq = 0c ) by A7, A11, A12, Lm1, Th42, COMPLEX1:13; ::_thesis: verum
end;

begin

theorem :: COMSEQ_3:49
for seq, seq1 being Complex_Sequence st seq is subsequence of seq1 holds
( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 )
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is subsequence of seq1 implies ( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 ) )
assume  seq is subsequence of seq1 ; ::_thesis: ( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 )
then consider Nseq being increasing sequence of NAT such that
A1: seq = seq1 * Nseq by VALUED_0:def_17;
 Re seq = (Re seq1) * Nseq by A1, Th22;
hence  Re seq is subsequence of Re seq1 ; ::_thesis: Im seq is subsequence of Im seq1
 Im seq = (Im seq1) * Nseq by A1, Th22;
hence  Im seq is subsequence of Im seq1 ; ::_thesis: verum
end;

theorem :: COMSEQ_3:50
for seq being Complex_Sequence st seq is bounded holds
ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is bounded implies ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) )
assume  seq is bounded ; ::_thesis: ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )
then consider r being Real such that
A1: 0 < r and
A2: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:8;
now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_((Re_seq)_._n)_<_r
let n be Element of NAT ; ::_thesis: abs ((Re seq) . n) < r
 ( abs ((Re seq) . n) = abs (Re (seq . n)) & abs (Re (seq . n)) <= |.(seq . n).| ) by Def5, Th13;
hence  abs ((Re seq) . n) < r by A2, XXREAL_0:2; ::_thesis: verum
end;
then  Re seq is bounded by A1, SEQ_2:3;
then consider rseq1 being Real_Sequence such that
A3: rseq1 is subsequence of Re seq and
A4: rseq1 is convergent by SEQ_4:40;
consider Nseq being increasing sequence of NAT such that
A5: rseq1 = (Re seq) * Nseq by A3, VALUED_0:def_17;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_|.((seq_*_Nseq)_._n).|_<_r
let n be Element of NAT ; ::_thesis: |.((seq * Nseq) . n).| < r
 |.((seq * Nseq) . n).| = |.(seq . (Nseq . n)).| by FUNCT_2:15;
hence  |.((seq * Nseq) . n).| < r by A2; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_((Im_(seq_*_Nseq))_._n)_<_r
let n be Element of NAT ; ::_thesis: abs ((Im (seq * Nseq)) . n) < r
 ( abs ((Im (seq * Nseq)) . n) = abs (Im ((seq * Nseq) . n)) & abs (Im ((seq * Nseq) . n)) <= |.((seq * Nseq) . n).| ) by Def6, Th13;
hence  abs ((Im (seq * Nseq)) . n) < r by A6, XXREAL_0:2; ::_thesis: verum
end;
then  Im (seq * Nseq) is bounded by A1, SEQ_2:3;
then consider rseq2 being Real_Sequence such that
A7: rseq2 is subsequence of Im (seq * Nseq) and
A8: rseq2 is convergent by SEQ_4:40;
consider Nseq1 being increasing sequence of NAT such that
A9: rseq2 = (Im (seq * Nseq)) * Nseq1 by A7, VALUED_0:def_17;
Re ((seq * Nseq) * Nseq1) = (Re (seq * Nseq)) * Nseq1 by Th22
.= rseq1 * Nseq1 by A5, Th22 ;
then A10: Re ((seq * Nseq) * Nseq1) is convergent by A4, SEQ_4:16;
 ( seq * Nseq is subsequence of seq & (seq * Nseq) * Nseq1 is subsequence of seq * Nseq ) by VALUED_0:def_17;
then A11: (seq * Nseq) * Nseq1 is subsequence of seq by VALUED_0:20;
 Im ((seq * Nseq) * Nseq1) is convergent by A8, A9, Th22;
hence  ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) by A11, A10, Th42; ::_thesis: verum
end;

definition
let seq be Complex_Sequence;
attrseq is summable  means :Def8: :: COMSEQ_3:def 8
 Partial_Sums seq is convergent ;
end;

:: deftheorem Def8 defines summable COMSEQ_3:def_8_:_
 for seq being Complex_Sequence holds
( seq is summable iff Partial_Sums seq is convergent );

set D = NAT --> 0c;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued summable for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is summable
proof
take  NAT --> 0c ; ::_thesis: NAT --> 0c is summable
take  0c ; :: according to COMSEQ_2:def_5,COMSEQ_3:def_8 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.(((Partial_Sums (NAT --> 0c)) . b3) - 0c).| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b2) - 0c).| ) )
assume A1: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b2) - 0c).| )
take  0 ; ::_thesis: for b1 being Element of NAT holds
( not 0 <= b1 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b1) - 0c).| )
 for n being Element of NAT holds (NAT --> 0c) . n = 0c by FUNCOP_1:7;
hence  for b1 being Element of NAT holds
( not 0 <= b1 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b1) - 0c).| ) by A1, Th24, COMPLEX1:44; ::_thesis: verum
end;
end;

registration
let seq be summable Complex_Sequence;
cluster Partial_Sums seq ->  convergent for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = Partial_Sums seq holds
b1 is convergent by Def8;
end;

definition
let seq be Complex_Sequence;
attrseq is absolutely_summable  means :Def9: :: COMSEQ_3:def 9
|.seq.| is summable ;
end;

:: deftheorem Def9 defines absolutely_summable COMSEQ_3:def_9_:_
 for seq being Complex_Sequence holds
( seq is absolutely_summable iff |.seq.| is summable );

theorem Th51: :: COMSEQ_3:51
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
seq is absolutely_summable
proof
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies seq is absolutely_summable )
assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: seq is absolutely_summable
take  0 ; :: according to SEQ_2:def_6,SERIES_1:def_2,COMSEQ_3:def_9 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs (((Partial_Sums |.seq.|) . b3) - 0) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((Partial_Sums |.seq.|) . b2) - 0) ) )
assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((Partial_Sums |.seq.|) . b2) - 0) )
take  0 ; ::_thesis: for b1 being Element of NAT holds
( not 0 <= b1 or not p <= abs (((Partial_Sums |.seq.|) . b1) - 0) )
let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= abs (((Partial_Sums |.seq.|) . m) - 0) )
abs (((Partial_Sums |.seq.|) . m) - 0) = abs (0 - 0) by A1, Th25
.= 0 by ABSVALUE:def_1 ;
hence  ( not 0 <= m or not p <= abs (((Partial_Sums |.seq.|) . m) - 0) ) by A2; ::_thesis: verum
end;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is absolutely_summable
proof
take  NAT --> 0c ; ::_thesis: NAT --> 0c is absolutely_summable
 for n being Element of NAT holds (NAT --> 0c) . n = 0c by FUNCOP_1:7;
hence  NAT --> 0c is absolutely_summable by Th51; ::_thesis: verum
end;
end;

registration
let seq be absolutely_summable Complex_Sequence;
cluster|.seq.| ->  summable for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = |.seq.| holds
b1 is summable by Def9;
end;

theorem Th52: :: COMSEQ_3:52
for seq being Complex_Sequence st seq is summable holds
( seq is convergent & lim seq = 0c )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable implies ( seq is convergent & lim seq = 0c ) )
assume A1: seq is summable ; ::_thesis: ( seq is convergent & lim seq = 0c )
then  Re (Partial_Sums seq) is convergent ;
then  Partial_Sums (Re seq) is convergent by Th26;
then A2: Re seq is summable by SERIES_1:def_2;
 Im (Partial_Sums seq) is convergent by A1;
then  Partial_Sums (Im seq) is convergent by Th26;
then A3: Im seq is summable by SERIES_1:def_2;
then  lim (Im seq) = 0 by SERIES_1:4;
then A4: Im (lim seq) = 0 by A2, A3, Th42;
 lim (Re seq) = 0 by A2, SERIES_1:4;
then  Re (lim seq) = 0 by A2, A3, Th42;
hence  ( seq is convergent & lim seq = 0c ) by A2, A3, A4, Lm1, Th42, COMPLEX1:13; ::_thesis: verum
end;

registration
cluster Function-like V18( NAT , COMPLEX ) summable  ->  convergent for Element of K19(K20(NAT,COMPLEX));
coherence
 for b1 being Complex_Sequence st b1 is summable holds
b1 is convergent by Th52;
end;

theorem Th53: :: COMSEQ_3:53
for seq being Complex_Sequence st seq is summable holds
( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable implies ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) ) )
A1: ( lim (Re (Partial_Sums seq)) = lim (Partial_Sums (Re seq)) & lim (Im (Partial_Sums seq)) = lim (Partial_Sums (Im seq)) ) by Th26;
assume A2: seq is summable ; ::_thesis: ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )
then  Re (Partial_Sums seq) is convergent ;
then A3: Partial_Sums (Re seq) is convergent by Th26;
 Im (Partial_Sums seq) is convergent by A2;
then A4: Partial_Sums (Im seq) is convergent by Th26;
 ( lim (Re (Partial_Sums seq)) = Re (lim (Partial_Sums seq)) & lim (Im (Partial_Sums seq)) = Im (lim (Partial_Sums seq)) ) by A2, Th41;
hence  ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) ) by A3, A4, A1, COMPLEX1:13, SERIES_1:def_2; ::_thesis: verum
end;

registration
let seq be summable Complex_Sequence;
cluster Re seq ->  summable for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Re seq holds
b1 is summable by Th53;
cluster Im seq ->  summable for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Im seq holds
b1 is summable by Th53;
end;

theorem Th54: :: COMSEQ_3:54
for seq1, seq2 being Complex_Sequence st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) )
assume A1: ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
then A2: (Partial_Sums seq1) + (Partial_Sums seq2) is convergent ;
A3: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by Th27;
Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th27
.= (lim (Partial_Sums seq1)) + (lim (Partial_Sums seq2)) by A1, COMSEQ_2:14 ;
hence  ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) by A2, A3, Def8; ::_thesis: verum
end;

theorem Th55: :: COMSEQ_3:55
for seq1, seq2 being Complex_Sequence st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) )
assume A1: ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
then A2: (Partial_Sums seq1) - (Partial_Sums seq2) is convergent ;
A3: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by Th28;
Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th28
.= (lim (Partial_Sums seq1)) - (lim (Partial_Sums seq2)) by A1, COMSEQ_2:26 ;
hence  ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) by A2, A3, Def8; ::_thesis: verum
end;

registration
let seq1, seq2 be summable Complex_Sequence;
clusterseq1 + seq2 ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = seq1 + seq2 holds
b1 is summable by Th54;
clusterseq1 - seq2 ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = seq1 - seq2 holds
b1 is summable by Th55;
end;

theorem Th56: :: COMSEQ_3:56
for seq being Complex_Sequence st seq is summable holds
for z being complex number holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable implies for z being complex number holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) )
assume A1: seq is summable ; ::_thesis: for z being complex number holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )
let z be complex number ; ::_thesis: ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )
A2: Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) by Th29;
Sum (z (#) seq) = lim (z (#) (Partial_Sums seq)) by Th29
.= z * (Sum seq) by A1, COMSEQ_2:18 ;
hence  ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) by A1, A2, Def8; ::_thesis: verum
end;

registration
let z be Element of COMPLEX ;
let seq be summable Complex_Sequence;
clusterz (#) seq ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = z (#) seq holds
b1 is summable by Th56;
end;

theorem Th57: :: COMSEQ_3:57
for seq being Complex_Sequence st Re seq is summable & Im seq is summable holds
( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )
proof
let seq be Complex_Sequence; ::_thesis: ( Re seq is summable & Im seq is summable implies ( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) ) )
assume that
A1: Re seq is summable and
A2: Im seq is summable ; ::_thesis: ( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )
 Partial_Sums (Im seq) is convergent by A2, SERIES_1:def_2;
then A3: Im (Partial_Sums seq) is convergent by Th26;
 Partial_Sums (Re seq) is convergent by A1, SERIES_1:def_2;
then A4: Re (Partial_Sums seq) is convergent by Th26;
then A5: lim (Im (Partial_Sums seq)) = Im (lim (Partial_Sums seq)) by A3, Th42;
A6: ( lim (Re (Partial_Sums seq)) = lim (Partial_Sums (Re seq)) & lim (Im (Partial_Sums seq)) = lim (Partial_Sums (Im seq)) ) by Th26;
 ( Partial_Sums seq is convergent & lim (Re (Partial_Sums seq)) = Re (lim (Partial_Sums seq)) ) by A4, A3, Th42;
hence  ( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) ) by A6, A5, Def8, COMPLEX1:13; ::_thesis: verum
end;

theorem Th58: :: COMSEQ_3:58
for seq being Complex_Sequence st seq is summable holds
for n being Element of NAT holds seq ^\ n is summable
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable implies for n being Element of NAT holds seq ^\ n is summable )
assume A1: seq is summable ; ::_thesis: for n being Element of NAT holds seq ^\ n is summable
let n be Element of NAT ; ::_thesis: seq ^\ n is summable
A2: ( Re (seq ^\ n) = (Re seq) ^\ n & Im (seq ^\ n) = (Im seq) ^\ n ) by Th23;
 ( (Re seq) ^\ n is summable & (Im seq) ^\ n is summable ) by A1, SERIES_1:12;
hence  seq ^\ n is summable by A2, Th57; ::_thesis: verum
end;

registration
let seq be summable Complex_Sequence;
let n be Element of NAT ;
clusterseq ^\ n ->  summable for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = seq ^\ n holds
b1 is summable by Th58;
end;

theorem :: COMSEQ_3:59
for seq being Complex_Sequence st ex n being Element of NAT st seq ^\ n is summable holds
seq is summable
proof
let seq be Complex_Sequence; ::_thesis: ( ex n being Element of NAT st seq ^\ n is summable implies seq is summable )
given n being Element of NAT  such that A1: seq ^\ n is summable ; ::_thesis: seq is summable
 Im (seq ^\ n) = (Im seq) ^\ n by Th23;
then A2: Im seq is summable by A1, SERIES_1:13;
 Re (seq ^\ n) = (Re seq) ^\ n by Th23;
then  Re seq is summable by A1, SERIES_1:13;
hence  seq is summable by A2, Th57; ::_thesis: verum
end;

theorem :: COMSEQ_3:60
for seq being Complex_Sequence st seq is summable holds
for n being Element of NAT holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable implies for n being Element of NAT holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) )
assume A1: seq is summable ; ::_thesis: for n being Element of NAT holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))
then  Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) by Th53;
then A2: ( Re (Sum seq) = Sum (Re seq) & Im (Sum seq) = Sum (Im seq) ) by COMPLEX1:12;
let n be Element of NAT ; ::_thesis: Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))
A3: Sum (seq ^\ (n + 1)) = (Sum (Re (seq ^\ (n + 1)))) + ((Sum (Im (seq ^\ (n + 1)))) * <i>) by A1, Th53;
A4: Sum (Im seq) = ((Partial_Sums (Im seq)) . n) + (Sum ((Im seq) ^\ (n + 1))) by A1, SERIES_1:15
.= ((Im (Partial_Sums seq)) . n) + (Sum ((Im seq) ^\ (n + 1))) by Th26
.= ((Im (Partial_Sums seq)) . n) + (Sum (Im (seq ^\ (n + 1)))) by Th23
.= ((Im (Partial_Sums seq)) . n) + (Im (Sum (seq ^\ (n + 1)))) by A3, COMPLEX1:12
.= (Im ((Partial_Sums seq) . n)) + (Im (Sum (seq ^\ (n + 1)))) by Def6
.= Im (((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))) by COMPLEX1:8 ;
Sum (Re seq) = ((Partial_Sums (Re seq)) . n) + (Sum ((Re seq) ^\ (n + 1))) by A1, SERIES_1:15
.= ((Re (Partial_Sums seq)) . n) + (Sum ((Re seq) ^\ (n + 1))) by Th26
.= ((Re (Partial_Sums seq)) . n) + (Sum (Re (seq ^\ (n + 1)))) by Th23
.= ((Re (Partial_Sums seq)) . n) + (Re (Sum (seq ^\ (n + 1)))) by A3, COMPLEX1:12
.= (Re ((Partial_Sums seq) . n)) + (Re (Sum (seq ^\ (n + 1)))) by Def5
.= Re (((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))) by COMPLEX1:8 ;
hence  Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) by A2, A4, COMPLEX1:def_3; ::_thesis: verum
end;

theorem Th61: :: COMSEQ_3:61
for seq being Complex_Sequence holds
( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )
proof
let seq be Complex_Sequence; ::_thesis: ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )
 for n being Element of NAT holds 0 <= |.seq.| . n by Lm3;
then  ( Partial_Sums |.seq.| is bounded_above iff |.seq.| is summable ) by SERIES_1:17;
hence  ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable ) by Def9; ::_thesis: verum
end;

registration
let seq be absolutely_summable Complex_Sequence;
cluster Partial_Sums |.seq.| ->  bounded_above for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Partial_Sums |.seq.| holds
b1 is bounded_above by Th61;
end;

theorem Th62: :: COMSEQ_3:62
for seq being Complex_Sequence holds
( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
now__::_thesis:_(_(_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).|_<_p_)_implies_seq_is_summable_)
assume  for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ; ::_thesis: seq is summable
then  Partial_Sums seq is convergent by Th46;
hence  seq is summable by Def8; ::_thesis: verum
end;
hence  ( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) by Th46; ::_thesis: verum
end;

theorem Th63: :: COMSEQ_3:63
for seq being Complex_Sequence st seq is absolutely_summable holds
seq is summable
proof
let seq be Complex_Sequence; ::_thesis: ( seq is absolutely_summable implies seq is summable )
assume A1: seq is absolutely_summable ; ::_thesis: seq is summable
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
then consider n being Element of NAT  such that
A2: for m being Element of NAT st n <= m holds
abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) < p by A1, SEQ_4:41;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
assume  n <= m ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
then A3: abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) < p by A2;
 |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by Th31;
hence  |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p by A3, XXREAL_0:2; ::_thesis: verum
end;
hence  seq is summable by Th62; ::_thesis: verum
end;

registration
cluster Function-like V18( NAT , COMPLEX ) absolutely_summable  ->  summable for Element of K19(K20(NAT,COMPLEX));
coherence
 for b1 being Complex_Sequence st b1 is absolutely_summable holds
b1 is summable by Th63;
end;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is absolutely_summable
proof
set C = the absolutely_summable Complex_Sequence;
take  the absolutely_summable Complex_Sequence ; ::_thesis: the absolutely_summable Complex_Sequence is absolutely_summable
thus  the absolutely_summable Complex_Sequence is absolutely_summable ; ::_thesis: verum
end;
end;

theorem Th64: :: COMSEQ_3:64
for z being Element of COMPLEX st |.z.| < 1 holds
( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) )
proof
let z be Element of COMPLEX ; ::_thesis: ( |.z.| < 1 implies ( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) ) )
set seq2 = NAT --> 1r;
deffunc H1( Element of NAT ) ->  Element of COMPLEX = z #N ($1 + 1);
consider seq1 being Complex_Sequence such that
A1: for n being Element of NAT holds seq1 . n = H1(n) from COMSEQ_1:sch_1();
assume A2: |.z.| < 1 ; ::_thesis: ( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) )
then A3: lim seq1 = 0c by A1, Th44;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_(z_GeoSeq))_._n_=_((1r_/_(1r_-_z))_(#)_((NAT_-->_1r)_-_seq1))_._n
let n be Element of NAT ; ::_thesis: (Partial_Sums (z GeoSeq)) . n = ((1r / (1r - z)) (#) ((NAT --> 1r) - seq1)) . n
thus (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z) by A2, Th36, COMPLEX1:48
.= (1r - (seq1 . n)) / (1r - z) by A1
.= (1r * (((NAT --> 1r) . n) - (seq1 . n))) / (1r - z) by COMPLEX1:def_4, FUNCOP_1:7
.= (1r / (1r - z)) * (((NAT --> 1r) . n) + (- (seq1 . n))) by XCMPLX_1:74
.= (1r / (1r - z)) * (((NAT --> 1r) . n) + ((- seq1) . n)) by VALUED_1:8
.= (1r / (1r - z)) * (((NAT --> 1r) - seq1) . n) by VALUED_1:1
.= ((1r / (1r - z)) (#) ((NAT --> 1r) - seq1)) . n by VALUED_1:6 ; ::_thesis: verum
end;
A5: for n being Element of NAT holds (NAT --> 1r) . n = 1r by FUNCOP_1:7;
then A6: NAT --> 1r is convergent by COMSEQ_2:9;
A7: seq1 is convergent by A2, A1, Th44;
then A8: (NAT --> 1r) - seq1 is convergent by A6;
hence  Partial_Sums (z GeoSeq) is convergent by A4, FUNCT_2:63; :: according to COMSEQ_3:def_8 ::_thesis: Sum (z GeoSeq) = 1r / (1r - z)
lim ((NAT --> 1r) - seq1) = (lim (NAT --> 1r)) - (lim seq1) by A7, A6, COMSEQ_2:26
.= 1r by A3, A5, COMSEQ_2:10 ;
then  lim ((1r / (1r - z)) (#) ((NAT --> 1r) - seq1)) = (1r / (1r - z)) * 1r by A8, COMSEQ_2:18
.= 1r / (1r - z) by COMPLEX1:def_4 ;
hence  Sum (z GeoSeq) = 1r / (1r - z) by A4, FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_3:65
for seq being Complex_Sequence
for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds
( seq is summable & Sum seq = (seq . 0) / (1r - z) )
proof
let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds
( seq is summable & Sum seq = (seq . 0) / (1r - z) )
let z be Element of COMPLEX ; ::_thesis: ( |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) implies ( seq is summable & Sum seq = (seq . 0) / (1r - z) ) )
assume that
A1: |.z.| < 1 and
A2: for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ; ::_thesis: ( seq is summable & Sum seq = (seq . 0) / (1r - z) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_seq)_._n_=_((seq_._0)_(#)_(Partial_Sums_(z_GeoSeq)))_._n
let n be Element of NAT ; ::_thesis: (Partial_Sums seq) . n = ((seq . 0) (#) (Partial_Sums (z GeoSeq))) . n
thus (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) by A1, A2, Th37, COMPLEX1:48
.= (seq . 0) * ((Partial_Sums (z GeoSeq)) . n) by A1, Th36, COMPLEX1:48
.= ((seq . 0) (#) (Partial_Sums (z GeoSeq))) . n by VALUED_1:6 ; ::_thesis: verum
end;
then A3: Partial_Sums seq = (seq . 0) (#) (Partial_Sums (z GeoSeq)) by FUNCT_2:63;
A4: z GeoSeq is summable by A1, Th64;
hence  seq is summable by A3, Def8; ::_thesis: Sum seq = (seq . 0) / (1r - z)
Sum seq = (seq . 0) * (Sum (z GeoSeq)) by A3, A4, COMSEQ_2:18
.= (seq . 0) * (1r / (1r - z)) by A1, Th64
.= ((seq . 0) * 1r) / (1r - z) by XCMPLX_1:74
.= (seq . 0) / (1r - z) by COMPLEX1:def_4 ;
hence  Sum seq = (seq . 0) / (1r - z) ; ::_thesis: verum
end;

theorem :: COMSEQ_3:66
for rseq1 being Real_Sequence
for seq2 being Complex_Sequence st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(seq2 . n).| <= rseq1 . n holds
seq2 is absolutely_summable
proof
let rseq1 be Real_Sequence; ::_thesis: for seq2 being Complex_Sequence st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(seq2 . n).| <= rseq1 . n holds
seq2 is absolutely_summable
let seq2 be Complex_Sequence; ::_thesis: ( rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(seq2 . n).| <= rseq1 . n implies seq2 is absolutely_summable )
assume that
A1: rseq1 is summable and
A2: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(seq2 . n).| <= rseq1 . n ; ::_thesis: seq2 is absolutely_summable
consider m being Element of NAT  such that
A3: for n being Element of NAT st m <= n holds
|.(seq2 . n).| <= rseq1 . n by A2;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_|.seq2.|_._n
let n be Element of NAT ; ::_thesis: 0 <= |.seq2.| . n
 |.(seq2 . n).| = |.seq2.| . n by VALUED_1:18;
hence  0 <= |.seq2.| . n by COMPLEX1:46; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
|.seq2.|_._n_<=_rseq1_._n
let n be Element of NAT ; ::_thesis: ( m <= n implies |.seq2.| . n <= rseq1 . n )
assume  m <= n ; ::_thesis: |.seq2.| . n <= rseq1 . n
then  |.(seq2 . n).| <= rseq1 . n by A3;
hence  |.seq2.| . n <= rseq1 . n by VALUED_1:18; ::_thesis: verum
end;
hence  |.seq2.| is summable by A1, A4, SERIES_1:19; :: according to COMSEQ_3:def_9 ::_thesis: verum
end;

theorem :: COMSEQ_3:67
for seq1, seq2 being Complex_Sequence st ( for n being Element of NAT holds
( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable holds
( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| )
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable implies ( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| ) )
assume  ( ( for n being Element of NAT holds
( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable ) ; ::_thesis: ( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| )
hence  ( |.seq1.| is summable & Sum |.seq1.| <= Sum |.seq2.| ) by SERIES_1:20; :: according to COMSEQ_3:def_9 ::_thesis: verum
end;

theorem :: COMSEQ_3:68
for seq being Complex_Sequence st ( for n being Element of NAT holds |.seq.| . n > 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds
not seq is absolutely_summable by SERIES_1:27;

theorem :: COMSEQ_3:69
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is absolutely_summable
proof
let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is absolutely_summable
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable )
assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is absolutely_summable
 for n being Element of NAT holds |.seq.| . n >= 0 by Lm3;
hence  |.seq.| is summable by A1, SERIES_1:28; :: according to COMSEQ_3:def_9 ::_thesis: verum
end;

theorem :: COMSEQ_3:70
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not |.seq.| is summable
proof
let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not |.seq.| is summable
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 implies not |.seq.| is summable )
assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 ) ; ::_thesis: not |.seq.| is summable
 for n being Element of NAT holds |.seq.| . n >= 0 by Lm3;
hence  not |.seq.| is summable by A1, SERIES_1:29; ::_thesis: verum
end;

theorem :: COMSEQ_3:71
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is absolutely_summable
proof
let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is absolutely_summable
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 implies not seq is absolutely_summable )
assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 ) ; ::_thesis: not seq is absolutely_summable
 for n being Element of NAT holds |.seq.| . n >= 0 by Lm3;
hence  not |.seq.| is summable by A1, SERIES_1:30; :: according to COMSEQ_3:def_9 ::_thesis: verum
end;

theorem :: COMSEQ_3:72
for rseq1 being Real_Sequence
for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds
( seq is absolutely_summable iff rseq1 is summable )
proof
let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds
( seq is absolutely_summable iff rseq1 is summable )
let seq be Complex_Sequence; ::_thesis: ( |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) implies ( seq is absolutely_summable iff rseq1 is summable ) )
assume  ( |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) ) ; ::_thesis: ( seq is absolutely_summable iff rseq1 is summable )
then  for n being Element of NAT holds
( |.seq.| is non-increasing & |.seq.| . n >= 0 & rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) by Lm3;
then  ( |.seq.| is summable iff rseq1 is summable ) by SERIES_1:31;
hence  ( seq is absolutely_summable iff rseq1 is summable ) by Def9; ::_thesis: verum
end;

theorem :: COMSEQ_3:73
for seq being Complex_Sequence
for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) holds
seq is absolutely_summable
proof
let seq be Complex_Sequence; ::_thesis: for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) holds
seq is absolutely_summable
let p be Real; ::_thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) implies seq is absolutely_summable )
assume  ( p > 1 & ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) ) ; ::_thesis: seq is absolutely_summable
then  |.seq.| is summable by SERIES_1:32;
hence  seq is absolutely_summable by Def9; ::_thesis: verum
end;

theorem :: COMSEQ_3:74
for seq being Complex_Sequence
for p being Real st p <= 1 & ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) holds
not seq is absolutely_summable by SERIES_1:33;

theorem :: COMSEQ_3:75
for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Element of NAT holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is absolutely_summable
proof
let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is absolutely_summable
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable )
assume that
A1: for n being Element of NAT holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) and
A2: ( rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is absolutely_summable
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_|.seq.|_._n_<>_0_&_rseq1_._n_=_(|.seq.|_._(n_+_1))_/_(|.seq.|_._n)_&_|.seq.|_._n_<>_0_&_rseq1_._n_=_((abs_|.seq.|)_._(n_+_1))_/_(|.seq.|_._n)_&_|.seq.|_._n_<>_0_&_rseq1_._n_=_((abs_|.seq.|)_._(n_+_1))_/_((abs_|.seq.|)_._n)_)
let n be Element of NAT ; ::_thesis: ( |.seq.| . n <> 0 & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) )
A3: ( seq . n <> 0c & |.seq.| . n = |.(seq . n).| ) by A1, VALUED_1:18;
hence  ( |.seq.| . n <> 0 & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) by A1, COMPLEX1:47; ::_thesis: ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) )
thus  ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / (|.seq.| . n) ) by A1, A3, COMPLEX1:47; ::_thesis: ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) )
thus  ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) ) by A1, A3, COMPLEX1:47; ::_thesis: verum
end;
then  |.seq.| is absolutely_summable by A2, SERIES_1:37;
hence  seq is absolutely_summable by Def9; ::_thesis: verum
end;

theorem :: COMSEQ_3:76
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n <> 0c ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds
not seq is absolutely_summable
proof
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0c ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 implies not seq is absolutely_summable )
assume that
A1: for n being Element of NAT holds seq . n <> 0c and
A2: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 ; ::_thesis: not seq is absolutely_summable
consider m being Element of NAT  such that
A3: for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 by A2;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_|.seq.|_._n_<>_0
let n be Element of NAT ; ::_thesis: |.seq.| . n <> 0
 seq . n <> 0c by A1;
then  |.(seq . n).| <> 0 by COMPLEX1:47;
hence  |.seq.| . n <> 0 by VALUED_1:18; ::_thesis: verum
end;
 for n being Element of NAT st n >= m holds
((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) >= 1 by A3;
hence  not |.seq.| is summable by A4, SERIES_1:39; :: according to COMSEQ_3:def_9 ::_thesis: verum
end;