:: Cauchy Sequence of Complex Unitary Space
::  by Yasumasa Suzuki and Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, CSSPACE, PRE_TOPC, NAT_1, SEQ_1, COMSEQ_1, CFUNCT_1,
      REAL_1, SUBSET_1, SUPINF_2, SERIES_1, ARYTM_3, FUNCT_1, CARD_1, ARYTM_1,
      RELAT_1, COMPLEX1, SEQ_2, CARD_3, ORDINAL2, BHSP_3, XXREAL_0, NORMSP_1,
      XXREAL_2, FUNCOP_1, VALUED_1, POWER, NEWTON, VALUED_0, INT_1, METRIC_1,
      CSSPACE2;
 notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, REAL_1,
      FUNCOP_1, VALUED_1, SEQ_1, SEQ_2, NAT_1, NEWTON, SERIES_1, VALUED_0,
      PRE_TOPC, COMSEQ_1, STRUCT_0, RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_4,
      POWER, INT_1, CFUNCT_1, COMSEQ_2, COMSEQ_3, CLVECT_1, CSSPACE, CLVECT_2,
      CSSPACE2;
 constructors REAL_1, COMSEQ_2, COMSEQ_3, BHSP_4, CLVECT_2, SEQ_1, SEQ_2,
      RELSET_1, ABIAN, VFUNCT_1;
 registrations ORDINAL1, FUNCT_2, XXREAL_0, XREAL_0, INT_1, MEMBERED, STRUCT_0,
      XBOOLE_0, VALUED_1, NUMBERS, VALUED_0, RELSET_1, FUNCOP_1, VFUNCT_1,
      XCMPLX_0, COMSEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions RLVECT_1, VALUED_1;
 theorems NAT_1, FUNCT_2, SEQ_1, SEQ_2, SEQM_3, SERIES_1, ABSVALUE, RLVECT_1,
      PREPOWER, POWER, INT_1, XCMPLX_1, CLVECT_1, CSSPACE, CLVECT_2, COMSEQ_1,
      COMSEQ_2, COMPLEX1, COMSEQ_3, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1,
      BHSP_4, BHSP_1, NORMSP_1, VALUED_1;
 schemes NAT_1, FUNCT_2;

begin :: Cauchy sequence of complex unitary space

reserve X for ComplexUnitarySpace;
reserve g for Point of X;
reserve seq, seq1, seq2 for sequence of X;
reserve Rseq for Real_Sequence;
reserve Cseq,Cseq1,Cseq2 for Complex_Sequence;
reserve z,z1,z2 for Complex;
reserve r for Real;
reserve k,n,m for Element of NAT;

deffunc 09(ComplexUnitarySpace) = 0.$1;

theorem Th1:
  Partial_Sums(seq1) + Partial_Sums(seq2) = Partial_Sums(seq1 + seq2)
proof
  set PSseq1 = Partial_Sums(seq1);
  set PSseq2 = Partial_Sums(seq2);
A1: now
    let n;
    thus (PSseq1 + PSseq2).(n + 1) = PSseq1.(n + 1) + PSseq2.(n + 1) by
NORMSP_1:def 2
      .= PSseq1.n + seq1.(n + 1) + PSseq2.(n + 1) by BHSP_4:def 1
      .= PSseq1.n + seq1.(n + 1) + (seq2.(n + 1) + PSseq2.n) by BHSP_4:def 1
      .= PSseq1.n + seq1.(n + 1) + seq2.(n + 1) + PSseq2.n by RLVECT_1:def 3
      .= PSseq1.n + (seq1.(n + 1) + seq2.(n + 1)) + PSseq2.n by RLVECT_1:def 3
      .= PSseq1.n + (seq1 + seq2).(n + 1) + PSseq2.n by NORMSP_1:def 2
      .= PSseq1.n + PSseq2.n + (seq1 + seq2).(n + 1) by RLVECT_1:def 3
      .= (PSseq1 + PSseq2).n + (seq1 + seq2).(n + 1) by NORMSP_1:def 2;
  end;
  (PSseq1 + PSseq2).0 = PSseq1.0 + PSseq2.0 by NORMSP_1:def 2
    .= seq1.0 + PSseq2.0 by BHSP_4:def 1
    .= seq1.0 + seq2.0 by BHSP_4:def 1
    .= (seq1 + seq2).0 by NORMSP_1:def 2;
  hence thesis by A1,BHSP_4:def 1;
end;

theorem Th2:
  Partial_Sums(seq1) - Partial_Sums(seq2) = Partial_Sums(seq1 - seq2)
proof
  set PSseq1 = Partial_Sums(seq1);
  set PSseq2 = Partial_Sums(seq2);
A1: now
    let n;
    thus (PSseq1 - PSseq2).(n + 1) = PSseq1.(n + 1) - PSseq2.(n + 1) by
NORMSP_1:def 3
      .= (PSseq1.n + seq1.(n + 1)) - PSseq2.(n + 1) by BHSP_4:def 1
      .= (PSseq1.n + seq1.(n + 1)) - (seq2.(n + 1) + PSseq2.n) by BHSP_4:def 1
      .= ((PSseq1.n + seq1.(n + 1)) - seq2.(n + 1)) - PSseq2.n by RLVECT_1:27
      .= (PSseq1.n + (seq1.(n + 1) - seq2.(n + 1))) - PSseq2.n by
RLVECT_1:def 3
      .= (PSseq1.n - PSseq2.n) + (seq1.(n + 1) - seq2.(n + 1)) by
RLVECT_1:def 3
      .= (PSseq1 - PSseq2).n + (seq1.(n + 1) - seq2.(n + 1)) by NORMSP_1:def 3
      .= (PSseq1 - PSseq2).n + (seq1 - seq2).(n + 1) by NORMSP_1:def 3;
  end;
  (PSseq1 - PSseq2).0 = (PSseq1).0 - (PSseq2).0 by NORMSP_1:def 3
    .= seq1.0 - (PSseq2).0 by BHSP_4:def 1
    .= seq1.0 - seq2.0 by BHSP_4:def 1
    .= (seq1 - seq2).0 by NORMSP_1:def 3;
  hence thesis by A1,BHSP_4:def 1;
end;

theorem Th3:
  Partial_Sums(z * seq) = z * Partial_Sums(seq)
proof
  set PSseq = Partial_Sums(seq);
A1: now
    let n;
    thus (z * PSseq).(n + 1) = z * PSseq.(n + 1) by CLVECT_1:def 14
      .= z * (PSseq.n + seq.(n + 1)) by BHSP_4:def 1
      .= z * PSseq.n + z * seq.(n + 1) by CLVECT_1:def 2
      .= (z * PSseq).n + z * seq.(n + 1) by CLVECT_1:def 14
      .= (z * PSseq).n + (z * seq).(n + 1) by CLVECT_1:def 14;
  end;
  (z * PSseq).0 = z * PSseq.0 by CLVECT_1:def 14
    .= z * seq.0 by BHSP_4:def 1
    .= (z * seq).0 by CLVECT_1:def 14;
  hence thesis by A1,BHSP_4:def 1;
end;

theorem
  Partial_Sums(- seq) = - Partial_Sums(seq)
proof
  Partial_Sums((-1r) * seq) = (-1r) * Partial_Sums(seq) by Th3;
  then Partial_Sums(- seq) = (-1r) * Partial_Sums(seq) by CSSPACE:70;
  hence thesis by CSSPACE:70;
end;

theorem
  z1 * Partial_Sums(seq1) + z2 * Partial_Sums(seq2) = Partial_Sums(z1*
  seq1 + z2*seq2)
proof
  thus z1 * Partial_Sums(seq1) + z2 * Partial_Sums(seq2) = Partial_Sums(z1 *
  seq1) + z2 * Partial_Sums(seq2) by Th3
    .= Partial_Sums(z1 * seq1) + Partial_Sums(z2 * seq2) by Th3
    .= Partial_Sums(z1 * seq1 + z2 * seq2) by Th1;
end;

definition
  let X, seq;
  attr seq is summable means
  :Def1:
  Partial_Sums(seq) is convergent;
  func Sum(seq) -> Point of X equals
  lim Partial_Sums(seq);
  correctness;
end;

theorem
  seq1 is summable & seq2 is summable implies seq1 + seq2 is summable &
  Sum(seq1 + seq2) = Sum(seq1) + Sum(seq2)
proof
  assume seq1 is summable & seq2 is summable;
  then
A1: Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent by Def1
;
  then Partial_Sums(seq1) + Partial_Sums(seq2) is convergent by CLVECT_2:3;
  then Partial_Sums(seq1 + seq2) is convergent by Th1;
  hence seq1 + seq2 is summable by Def1;
  thus Sum(seq1 + seq2) = lim (Partial_Sums(seq1) + Partial_Sums(seq2)) by Th1
    .= Sum(seq1) + Sum(seq2) by A1,CLVECT_2:13;
end;

theorem
  seq1 is summable & seq2 is summable implies seq1 - seq2 is summable &
  Sum(seq1 - seq2) = Sum(seq1) - Sum(seq2)
proof
  assume seq1 is summable & seq2 is summable;
  then
A1: Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent by Def1
;
  then Partial_Sums(seq1) - Partial_Sums(seq2) is convergent by CLVECT_2:4;
  then Partial_Sums(seq1 - seq2) is convergent by Th2;
  hence seq1 - seq2 is summable by Def1;
  thus Sum(seq1 - seq2) = lim (Partial_Sums(seq1) - Partial_Sums(seq2)) by Th2
    .= Sum(seq1) - Sum(seq2) by A1,CLVECT_2:14;
end;

theorem
  seq is summable implies z * seq is summable & Sum(z*seq) = z * Sum(seq )
proof
  assume seq is summable;
  then
A1: Partial_Sums(seq) is convergent by Def1;
  then z * Partial_Sums(seq) is convergent by CLVECT_2:5;
  then Partial_Sums(z * seq) is convergent by Th3;
  hence z * seq is summable by Def1;
  thus Sum(z * seq) = lim (z * Partial_Sums(seq)) by Th3
    .= z * Sum(seq) by A1,CLVECT_2:15;
end;

theorem Th9:
  seq is summable implies seq is convergent & lim seq = 0.X
proof
  set PSseq = Partial_Sums(seq);
  now
    let n;
    (PSseq).(n + 1) = (PSseq).n + seq.(n + 1) by BHSP_4:def 1
      .= (PSseq).n + (seq ^\1).n by NAT_1:def 3;
    hence (PSseq ^\1).n = (PSseq).n + (seq ^\1).n by NAT_1:def 3;
  end;
  then
A1: (PSseq ^\1) = PSseq + seq ^\1 by NORMSP_1:def 2;
  now
    let n;
    thus (seq ^\1 + (PSseq - PSseq)).n = (seq ^\1).n + (PSseq - PSseq).n by
NORMSP_1:def 2
      .= (seq ^\1).n + (PSseq.n - PSseq.n) by NORMSP_1:def 3
      .= (seq ^\1).n + 09(X) by RLVECT_1:15
      .= (seq ^\1).n by RLVECT_1:4;
  end;
  then seq ^\1 + (PSseq - PSseq) = seq ^\1 by FUNCT_2:63;
  then
A2: seq ^\1 = PSseq ^\1 - PSseq by A1,CSSPACE:76;
  assume seq is summable;
  then
A3: PSseq is convergent by Def1;
  then
A4: PSseq ^\1 is convergent by CLVECT_2:90;
  then
A5: seq ^\1 is convergent by A3,A2,CLVECT_2:4;
  hence seq is convergent by CLVECT_2:91;
  lim(PSseq ^\1) = lim(PSseq) by A3,CLVECT_2:90;
  then lim(PSseq ^\1 - PSseq) = lim(PSseq) - lim(PSseq) by A3,A4,CLVECT_2:14
    .= 09(X) by RLVECT_1:15;
  hence thesis by A2,A5,CLVECT_2:84,91;
end;

theorem Th10:
  for X being ComplexHilbertSpace, seq being sequence of X
  holds seq is summable iff for r st r > 0 ex k
st for n, m st n >= k & m >= k holds ||.(Partial_Sums(seq)).n - (Partial_Sums(
  seq)).m.|| < r
proof
  let X be ComplexHilbertSpace, seq be sequence of X;
  set PSseq = Partial_Sums(seq);
  thus seq is summable implies for r st r > 0 ex k st for n, m st n >= k & m
  >= k holds ||.(PSseq).n - (PSseq).m.|| < r
  proof
    assume seq is summable;
    then PSseq is convergent by Def1;
    then PSseq is Cauchy by CLVECT_2:65;
    hence thesis by CLVECT_2:58;
  end;
  thus ( for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.(
  PSseq).n - (PSseq).m.|| < r ) implies seq is summable
  proof
    assume for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.(PSseq
    ).n - (PSseq).m.|| < r;
    then PSseq is Cauchy by CLVECT_2:58;
    then PSseq is convergent by CLVECT_2:def 11;
    hence thesis by Def1;
  end;
end;

theorem
  seq is summable implies Partial_Sums(seq) is bounded
proof
  assume seq is summable;
  then Partial_Sums(seq) is convergent by Def1;
  hence thesis by CLVECT_2:80;
end;

theorem Th12:
  (for n holds seq1.n = seq.0) implies Partial_Sums(seq^\1) = (
  Partial_Sums(seq)^\1) - seq1
proof
  assume
A1: for n holds seq1.n = seq.0;
A2: now
    let n;
    thus ((Partial_Sums(seq)^\1) - seq1).(n + 1) = (Partial_Sums(seq)^\1).(n +
    1) - seq1.(n + 1) by NORMSP_1:def 3
      .= (Partial_Sums(seq)^\1).(n + 1) - seq.0 by A1
      .= Partial_Sums(seq).(n + 1 + 1) - seq.0 by NAT_1:def 3
      .= seq.(n+1+1) + Partial_Sums(seq).(n + 1) - seq.0 by BHSP_4:def 1
      .= seq.(n+1+1) + Partial_Sums(seq).(n + 1) - seq1.n by A1
      .= seq.(n+1+1) + (Partial_Sums(seq).(n + 1) - seq1.n) by RLVECT_1:def 3
      .= seq.(n+1+1) + ((Partial_Sums(seq)^\1).n - seq1.n) by NAT_1:def 3
      .= seq.(n+1+1) + ((Partial_Sums(seq)^\1) - seq1).n by NORMSP_1:def 3
      .= ((Partial_Sums(seq)^\1) - seq1).n + (seq^\1).(n + 1) by NAT_1:def 3;
  end;
  ((Partial_Sums(seq)^\1) - seq1).0 = (Partial_Sums(seq)^\1).0 - seq1.0 by
NORMSP_1:def 3
    .= (Partial_Sums(seq)^\1).0 - seq.0 by A1
    .= Partial_Sums(seq).(0 + 1) - seq.0 by NAT_1:def 3
    .= Partial_Sums(seq).0 + seq.(0 + 1) - seq.0 by BHSP_4:def 1
    .= seq.(0 + 1) + seq.0 - seq.0 by BHSP_4:def 1
    .= seq.(0 + 1) + (seq.0 - seq.0) by RLVECT_1:def 3
    .= seq.(0 + 1) + 09(X) by RLVECT_1:15
    .= seq.(0 + 1) by RLVECT_1:4
    .= (seq^\1).0 by NAT_1:def 3;
  hence thesis by A2,BHSP_4:def 1;
end;

theorem Th13:
  seq is summable implies for k holds seq^\k is summable
proof
  defpred P[Element of NAT] means seq^\($1) is summable;
A1: for k st P[k] holds P[k+1]
  proof
    let k;
    reconsider seq1 = NAT --> (seq^\k).0 as sequence of X;
    assume seq^\k is summable;
    then Partial_Sums(seq^\k) is convergent by Def1;
    then
A2: Partial_Sums(seq^\k)^\1 is convergent by CLVECT_2:90;
    for m holds seq1.m = (seq^\k).0 by FUNCOP_1:7;
    then
    seq1 is convergent & Partial_Sums(seq^\k^\1) = (Partial_Sums(seq^\k)^\
    1) - seq1 by Th12,CLVECT_2:1;
    then
    seq^\(k+1)=(seq^\k)^\1 & Partial_Sums(seq^\k^\1) is convergent by A2,
CLVECT_2:4,NAT_1:48;
    hence thesis by Def1;
  end;
  assume seq is summable;
  then
A3: P[0] by NAT_1:47;
  thus for k holds P[k] from NAT_1:sch 1(A3,A1);
end;

theorem
  (ex k st seq^\k is summable) implies seq is summable
proof
  given k such that
A1: seq^\k is summable;
  seq^\k^\1 is summable by A1,Th13;
  then
A2: Partial_Sums(seq^\k^\1) is convergent by Def1;
  reconsider seq1 = NAT --> Partial_Sums(seq).k as sequence of X;
  defpred P[Element of NAT] means (Partial_Sums(seq)^\(k+1)).$1 = Partial_Sums
  (seq^\(k+1)).$1 + seq1.$1;
A3: Partial_Sums(seq^\(k+1)).0 = (seq^\(k+1)).0 by BHSP_4:def 1
    .= seq.(0+(k+1)) by NAT_1:def 3
    .= seq.(k+1);
A4: now
    let m;
    assume
A5: P[m];
    Partial_Sums(seq^\(k+1)).(m+1) + seq1.(m+1) = seq1.(m+1) + (
    Partial_Sums(seq^\(k+1)).m + (seq^\(k+1)).(m+1)) by BHSP_4:def 1
      .= seq1.(m+1) + Partial_Sums(seq^\(k+1)).m + (seq^\(k+1)).(m+1) by
RLVECT_1:def 3
      .= Partial_Sums(seq).k + Partial_Sums(seq^\(k+1)).m + (seq^\(k+1)).(m+
    1) by FUNCOP_1:7
      .= (Partial_Sums(seq)^\(k+1)).m + (seq^\(k+1)).(m+1) by A5,FUNCOP_1:7
      .= Partial_Sums(seq).(m+(k+1)) + (seq^\(k+1)).(m+1) by NAT_1:def 3
      .= Partial_Sums(seq).(m+(k+1)) + seq.(m+1+(k+1)) by NAT_1:def 3
      .= Partial_Sums(seq).(m+(k+1)+1) by BHSP_4:def 1
      .= Partial_Sums(seq).(m+1+(k+1))
      .= (Partial_Sums(seq)^\(k+1)).(m+1) by NAT_1:def 3;
    hence P[m+1];
  end;
  (Partial_Sums(seq)^\(k+1)).0 = Partial_Sums(seq).(0+(k+1)) by NAT_1:def 3
    .= Partial_Sums(seq).k + seq.(k+1) by BHSP_4:def 1
    .= Partial_Sums(seq^\(k+1)).0 + seq1.0 by A3,FUNCOP_1:7;
  then
A6: P[0];
  for m holds P[m] from NAT_1:sch 1(A6,A4);
  then
A7: Partial_Sums(seq)^\(k+1) = Partial_Sums(seq^\(k+1)) + seq1 by
NORMSP_1:def 2
    .= Partial_Sums((seq^\k)^\1) + seq1 by NAT_1:48;
  seq1 is convergent by CLVECT_2:1;
  then Partial_Sums(seq)^\(k+1) is convergent by A2,A7,CLVECT_2:3;
  then Partial_Sums(seq) is convergent by CLVECT_2:91;
  hence thesis by Def1;
end;

definition
  let X, seq, n;
  func Sum(seq,n) -> Point of X equals
  Partial_Sums(seq).n;
  correctness;
end;

theorem
  Sum(seq, 0) = seq.0 by BHSP_4:def 1;

theorem Th16:
  Sum(seq,1) = Sum(seq,0) + seq.1
proof
  Partial_Sums(seq).1 = Partial_Sums(seq).0 + seq.(0 + 1) by BHSP_4:def 1
    .= Partial_Sums(seq).0 + seq.1;
  hence thesis;
end;

theorem Th17:
  Sum(seq,1) = seq.0 + seq.1
proof
  thus Sum(seq,1) = Sum(seq,0) + seq.1 by Th16
    .= seq.0 + seq.1 by BHSP_4:def 1;
end;

theorem
  Sum(seq,n+1) = Sum(seq,n) + seq.(n+1) by BHSP_4:def 1;

theorem Th19:
  seq.(n+1) = Sum(seq,n+1) - Sum(seq,n)
proof
  thus Sum(seq,n+1)-Sum(seq,n) = (seq.(n+1)+Sum(seq,n)) - Sum(seq,n) by
BHSP_4:def 1
    .= seq.(n+1) + (Sum(seq,n)-Sum(seq,n)) by RLVECT_1:def 3
    .= seq.(n+1) + 0.X by RLVECT_1:15
    .= seq.(n+1) by RLVECT_1:4;
end;

theorem
  seq.1 = Sum(seq,1) - Sum(seq,0)
proof
  seq.(0+1) = Sum(seq,0+1) - Sum(seq,0) by Th19;
  hence thesis;
end;

definition
  let X, seq, n, m;
  func Sum(seq, n, m) -> Point of X equals
  Sum(seq,n) - Sum(seq,m);
  correctness;
end;

theorem
  Sum(seq,1,0) = seq.1
proof
  Sum(seq,1,0) = (seq.0 + seq.1) - Sum(seq,0) by Th17
    .= (seq.1 + seq.0) - seq.0 by BHSP_4:def 1
    .= seq.1 + (seq.0 - seq.0) by RLVECT_1:def 3
    .= seq.1 + 09(X) by RLVECT_1:15;
  hence thesis by RLVECT_1:4;
end;

theorem
  Sum(seq,n+1,n) = seq.(n+1) by Th19;

theorem Th23:
  for X being ComplexHilbertSpace, seq being sequence of X
  holds seq is summable iff for r st r > 0 ex k
  st for n, m st n >= k & m >= k holds ||.Sum(seq, n) - Sum(seq, m).|| < r
proof
  let X be ComplexHilbertSpace, seq be sequence of X;
  thus seq is summable implies for r st r > 0 ex k st for n, m st n >= k & m
  >= k holds ||.Sum(seq, n) - Sum(seq, m).|| < r
  proof
    assume
A1: seq is summable;
    now
      let r;
      assume r > 0;
      then consider k such that
A2:   for n, m st n >= k & m >= k holds ||.(Partial_Sums(seq)).n - (
      Partial_Sums(seq)).m.|| < r by A1,Th10;
      take k;
      let n, m;
      assume n >= k & m >= k;
      hence ||.Sum(seq, n) - Sum(seq, m).|| < r by A2;
    end;
    hence thesis;
  end;
  thus ( for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.Sum(
  seq, n) - Sum(seq, m).|| < r ) implies seq is summable
  proof
    assume
A3: for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.Sum(
    seq, n) - Sum(seq, m).|| < r;
    now
      let r;
      assume r > 0;
      then consider k such that
A4:   for n, m st n >= k & m >= k holds ||.Sum(seq, n) - Sum(seq, m)
      .|| < r by A3;
      take k;
      let n, m;
      assume n >= k & m >= k;
      then ||.Sum(seq, n) - Sum(seq, m).|| < r by A4;
      hence ||.(Partial_Sums(seq)).n - (Partial_Sums(seq)).m.|| < r;
    end;
    hence thesis by Th10;
  end;
end;

theorem
  for X being ComplexHilbertSpace, seq being sequence of X
  holds seq is summable iff for r st r > 0 ex k st for
  n, m st n>=k & m>=k holds ||.Sum(seq, n, m).|| < r
proof
  let X be ComplexHilbertSpace, seq be sequence of X;
  thus seq is summable implies for r st r > 0 ex k st for n, m st n >= k & m
  >= k holds ||.Sum(seq, n, m).|| < r
  proof
    assume
A1: seq is summable;
    now
      let r;
      assume r > 0;
      then consider k such that
A2:   for n, m st n >= k & m >= k holds ||.Sum(seq, n) - Sum(seq, m)
      .|| < r by A1,Th23;
      take k;
      let n, m;
      assume n >= k & m >= k;
      hence ||.Sum(seq, n, m).|| < r by A2;
    end;
    hence thesis;
  end;
  thus ( for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.Sum(
  seq, n, m).|| < r ) implies seq is summable
  proof
    assume
A3: for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.Sum(
    seq, n, m).|| < r;
    now
      let r;
      assume r > 0;
      then consider k such that
A4:   for n, m st n >= k & m >= k holds ||.Sum(seq, n, m).|| < r by A3;
      take k;
      let n, m;
      assume n >= k & m >= k;
      then ||.Sum(seq, n, m).|| < r by A4;
      hence ||.Sum(seq, n) - Sum(seq, m).|| < r;
    end;
    hence thesis by Th23;
  end;
end;

definition
  let Cseq, n;
  func Sum(Cseq,n) -> Complex equals
  Partial_Sums(Cseq).n;
  correctness;
end;

definition
  let Cseq, n,m;
  func Sum(Cseq,n,m) -> Complex equals
  Sum(Cseq,n) - Sum(Cseq,m);
  correctness;
end;

definition
  let X, seq;
  attr seq is absolutely_summable means
  :Def7:
  ||.seq.|| is summable;
end;

theorem
  seq1 is absolutely_summable & seq2 is absolutely_summable implies seq1
  + seq2 is absolutely_summable
proof
A1: for n holds ||.seq1 + seq2.||.n >= 0 & ||.seq1 + seq2.||.n <= (||.seq1
  .|| + ||.seq2.||).n
  proof
    let n;
    ||.seq1 + seq2.||.n = ||.(seq1 + seq2).n.|| by CLVECT_2:def 3;
    hence ||.seq1 + seq2.||.n >= 0 by CSSPACE:44;
    ||.seq1+seq2.||.n = ||.(seq1 + seq2).n.|| by CLVECT_2:def 3
      .= ||.(seq1).n + (seq2).n.|| by NORMSP_1:def 2;
    then ||.seq1+seq2.||.n <= ||.(seq1).n.|| + ||.(seq2).n.|| by CSSPACE:46;
    then ||.seq1+seq2.||.n <= ||.seq1.||.n + ||.(seq2).n.|| by CLVECT_2:def 3;
    then ||.seq1 + seq2.||.n <= ||.seq1.||.n + ||.seq2.||.n by CLVECT_2:def 3;
    hence ||.seq1 + seq2.||.n <= (||.seq1.|| + ||.seq2.||).n by SEQ_1:7;
  end;
  assume seq1 is absolutely_summable & seq2 is absolutely_summable;
  then ||.seq1.|| is summable & ||.seq2.|| is summable by Def7;
  then ||.seq1.|| + ||.seq2.|| is summable by SERIES_1:7;
  then ||.seq1 + seq2.|| is summable by A1,SERIES_1:20;
  hence thesis by Def7;
end;

theorem
  seq is absolutely_summable implies z * seq is absolutely_summable
proof
A1: for n holds ||.z * seq.||.n >= 0 & ||.z * seq.||.n <= (|.z.| (#) ||.seq
  .||).n
  proof
    let n;
    ||.z * seq.||.n = ||.(z * seq).n.|| by CLVECT_2:def 3;
    hence ||.z * seq.||.n >= 0 by CSSPACE:44;
    ||.z * seq.||.n = ||.(z * seq).n.|| by CLVECT_2:def 3
      .= ||.z * seq.n.|| by CLVECT_1:def 14
      .= |.z.| * ||.seq.n.|| by CSSPACE:43
      .= |.z.| * ||.seq.||.n by CLVECT_2:def 3
      .= (|.z.| (#) ||.seq.||).n by SEQ_1:9;
    hence ||.z * seq.||.n <= (|.z.| (#) ||.seq.||).n;
  end;
  assume seq is absolutely_summable;
  then ||.seq.|| is summable by Def7;
  then |.z.| (#) ||.seq.|| is summable by SERIES_1:10;
  then ||.z * seq.|| is summable by A1,SERIES_1:20;
  hence thesis by Def7;
end;

theorem
  ( for n holds ||.seq.||.n <= Rseq.n ) & Rseq is summable implies seq
  is absolutely_summable
proof
A1: for n holds ||.seq.||.n >= 0
  proof
    let n;
    ||.seq.||.n = ||.seq.n.|| by CLVECT_2:def 3;
    hence thesis by CSSPACE:44;
  end;
  assume ( for n holds ||.seq.||.n <= Rseq.n)& Rseq is summable;
  then ||.seq.|| is summable by A1,SERIES_1:20;
  hence thesis by Def7;
end;

theorem
  ( for n holds seq.n <> 0.X & Rseq.n = ||.seq.(n+1).||/||.seq.n.|| ) &
  Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable
proof
  assume that
A1: for n holds seq.n <> 09(X) & Rseq.n = ||.seq.(n+1).||/||.seq.n.|| and
A2: Rseq is convergent & lim Rseq < 1;
  for n holds ||.seq.||.n > 0 & Rseq.n = ||.seq.||.(n+1)/||.seq.||.n
  proof
    let n;
    seq.n <> 09(X) by A1;
    then
A3: ||.seq.n.|| <> 0 by CSSPACE:42;
    ||.seq.n.|| >= 0 by CSSPACE:44;
    hence ||.seq.||.n > 0 by A3,CLVECT_2:def 3;
    Rseq.n = ||.seq.(n+1).||/||.seq.n.|| by A1
      .= ||.seq.||.(n+1)/||.seq.n.|| by CLVECT_2:def 3;
    hence Rseq.n = ||.seq.||.(n+1)/||.seq.||.n by CLVECT_2:def 3;
  end;
  then ||.seq.|| is summable by A2,SERIES_1:26;
  hence thesis by Def7;
end;

theorem Th29:
  r > 0 & ( ex m st for n st n >= m holds ||.seq.n.|| >= r)
  implies not seq is convergent or lim seq <> 0.X
proof
  assume
A1: r > 0;
  given m such that
A2: for n st n >= m holds ||.seq.n.|| >= r;
  now
    per cases;
    suppose
      not seq is convergent;
      hence thesis;
    end;
    suppose
A3:   seq is convergent;
      now
        assume lim seq = 09(X);
        then consider k such that
A4:     for n st n >= k holds ||.seq.n - 09(X).|| < r by A1,A3,CLVECT_2:19;
        now
          let n;
          assume
A5:       n >= m+k;
          m+k >= k by NAT_1:11;
          then n >= k by A5,XXREAL_0:2;
          then ||.seq.n - 09(X).|| < r by A4;
          then
A6:       ||.seq.n.|| < r by RLVECT_1:13;
          m+k >= m by NAT_1:11;
          then n >= m by A5,XXREAL_0:2;
          hence contradiction by A2,A6;
        end;
        hence contradiction;
      end;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem Th30:
  ( for n holds seq.n <> 0.X ) & ( ex m st for n st n >= m holds
  ||.seq.(n+1).||/||.seq.n.|| >= 1 ) implies not seq is summable
proof
  assume
A1: for n holds seq.n <> 09(X);
  given m such that
A2: for n st n >= m holds ||.seq.(n+1).||/||.seq.n.|| >= 1;
A3: now
    defpred P[Element of NAT] means ||.seq.(m+$1).|| >= ||.seq.m.||;
    let n;
A4: for k st P[k] holds P[k+1]
    proof
      let k;
      assume
A5:   ||.seq.(m+k).|| >= ||.seq.m.||;
      seq.(m+k) <> 09(X) by A1;
      then
A6:   ||.seq.(m+k).|| <> 0 by CSSPACE:42;
      ||.seq.(m+k+1).||/||.seq.(m+k).|| >= 1 & ||.seq.(m+k).|| >= 0 by A2,
CSSPACE:44,NAT_1:11;
      then ||.seq.(m+k+1).|| >= ||.seq.(m+k).|| by A6,XREAL_1:191;
      hence thesis by A5,XXREAL_0:2;
    end;
A7: P[0];
A8: for k holds P[k] from NAT_1:sch 1(A7,A4);
    assume n >= m;
    then consider k being Nat such that
A9: n = m + k by NAT_1:10;
    k in NAT by ORDINAL1:def 12;
    hence ||.seq.n.|| >= ||.seq.m.|| by A8,A9;
  end;
  seq.m <> 09(X) by A1;
  then ||.seq.m.|| <> 0 by CSSPACE:42;
  then ||.seq.m.|| > 0 by CSSPACE:44;
  then not seq is convergent or lim seq <> 09(X) by A3,Th29;
  hence thesis by Th9;
end;

theorem
  (for n holds seq.n <> 0.X) & (for n holds Rseq.n = ||.seq.(n+1).||/||.
  seq.n.||) & Rseq is convergent & lim Rseq > 1 implies not seq is summable
proof
  assume that
A1: for n holds seq.n <> 09(X) and
A2: for n holds Rseq.n = ||.seq.(n+1).||/||.seq.n.|| and
A3: Rseq is convergent and
A4: lim Rseq > 1;
  lim Rseq - 1 > 0 by A4,XREAL_1:50;
  then consider m such that
A5: for n st n >= m holds abs(Rseq.n - lim Rseq) < lim Rseq - 1 by A3,
SEQ_2:def 7;
  now
    let n;
A6: m + 1 >= m by NAT_1:11;
A7: Rseq.n = ||.seq.(n+1).||/||.seq.n.|| by A2;
    assume n >= m + 1;
    then n >= m by A6,XXREAL_0:2;
    then
    abs(||.seq.(n+1).||/||.seq.n.|| - lim Rseq) < lim Rseq - 1 by A5,A7;
    then - (lim Rseq - 1) < ||.seq.(n+1).||/||.seq.n.|| - lim Rseq by SEQ_2:1;
    then 1 - lim Rseq + lim Rseq < ||.seq.(n+1).||/||.seq.n.|| - lim Rseq+lim
    Rseq by XREAL_1:6;
    hence ||.seq.(n+1).||/||.seq.n.|| >= 1;
  end;
  hence thesis by A1,Th30;
end;

theorem
  ( for n holds Rseq.n = n-root (||.seq.n.||) ) & Rseq is convergent &
  lim Rseq < 1 implies seq is absolutely_summable
proof
  assume that
A1: for n holds Rseq.n = n-root (||.seq.n.||) and
A2: Rseq is convergent & lim Rseq < 1;
  for n holds ||.seq.||.n >= 0 & Rseq.n = n-root (||.seq.||.n)
  proof
    let n;
    ||.seq.||.n = ||.seq.n.|| by CLVECT_2:def 3;
    hence ||.seq.||.n >= 0 by CSSPACE:44;
    Rseq.n = n-root (||.seq.n.||) by A1;
    hence Rseq.n = n-root (||.seq.||.n) by CLVECT_2:def 3;
  end;
  then ||.seq.|| is summable by A2,SERIES_1:28;
  hence thesis by Def7;
end;

theorem
  (for n holds Rseq.n = n-root (||.seq.||.n)) & (ex m st for n st n >= m
  holds Rseq.n >= 1) implies not seq is summable
proof
  assume
A1: for n holds Rseq.n = n-root (||.seq.||.n);
  given m such that
A2: for n st n >= m holds Rseq.n >= 1;
  now
    let n;
    assume
A3: n >= m+1;
    m + 1 >= 1 by NAT_1:11;
    then
A4: n >= 1 by A3,XXREAL_0:2;
    m+1 >= m by NAT_1:11;
    then
A5: n>=m by A3,XXREAL_0:2;
    Rseq.n = n-root (||.seq.||.n) by A1
      .= n-root ||.seq.n.|| by CLVECT_2:def 3;
    then ||.seq.n.|| >= 0 & n-root ||.seq.n.|| |^ n >= 1 by A2,A5,CSSPACE:44
,PREPOWER:11;
    hence ||.seq.n.|| >= 1 by A4,POWER:4;
  end;
  then not seq is convergent or lim seq <> 09(X) by Th29;
  hence thesis by Th9;
end;

theorem
  (for n holds Rseq.n = n-root (||.seq.||.n)) & Rseq is convergent & lim
  Rseq > 1 implies not seq is summable
proof
  assume that
A1: for n holds Rseq.n = n-root (||.seq.||.n) and
A2: Rseq is convergent and
A3: lim Rseq > 1;
  lim Rseq - 1 > 0 by A3,XREAL_1:50;
  then consider m such that
A4: for n st n >= m holds abs(Rseq.n - lim Rseq) < lim Rseq - 1 by A2,
SEQ_2:def 7;
  now
    let n;
    assume
A5: n >= m + 1;
A6: Rseq.n = n-root (||.seq.||.n) by A1
      .= n-root ||.seq.n.|| by CLVECT_2:def 3;
    m + 1 >= m by NAT_1:11;
    then n >= m by A5,XXREAL_0:2;
    then abs(n-root ||.seq.n.|| - lim Rseq) < lim Rseq - 1 by A4,A6;
    then - (lim Rseq - 1) < n-root ||.seq.n.|| - lim Rseq by SEQ_2:1;
    then
    1 - lim Rseq + lim Rseq < n-root ||.seq.n.|| - lim Rseq + lim Rseq by
XREAL_1:6;
    then
A7: ||.seq.n.|| >= 0 & n-root ||.seq.n.|| |^ n >= 1 by CSSPACE:44,PREPOWER:11;
    m + 1 >= 1 by NAT_1:11;
    then n >= 1 by A5,XXREAL_0:2;
    hence ||.seq.n.|| >= 1 by A7,POWER:4;
  end;
  then not seq is convergent or lim seq <> 09(X) by Th29;
  hence thesis by Th9;
end;

theorem Th35:
  Partial_Sums(||.seq.||) is non-decreasing
proof
  now
    let n;
    ||.seq.(n+1).|| >= 0 by CSSPACE:44;
    then ||.seq.||.(n+1) >= 0 by CLVECT_2:def 3;
    then
    0 + Partial_Sums(||.seq.||).n <= ||.seq.||.(n+1) + Partial_Sums(||.seq
    .||).n by XREAL_1:6;
    hence Partial_Sums(||.seq.||).n <= Partial_Sums(||.seq.||).(n+1) by
SERIES_1:def 1;
  end;
  hence thesis by SEQM_3:def 8;
end;

theorem
  for n holds Partial_Sums(||.seq.||).n >= 0
proof
  let n;
  ||.(seq.0).|| >= 0 by CSSPACE:44;
  then ||.seq.||.0 >= 0 by CLVECT_2:def 3;
  then Partial_Sums(||.seq.||).0 >= 0 by SERIES_1:def 1;
  hence thesis by Th35,SEQM_3:11;
end;

theorem Th37:
  for n holds ||.Partial_Sums(seq).n.|| <= Partial_Sums(||.seq.||) .n
proof
  defpred P[Element of NAT] means ||.Partial_Sums(seq).$1.|| <= Partial_Sums(
  ||.seq.||).$1;
A1: now
    let n;
    Partial_Sums(seq).(n+1) = Partial_Sums(seq).n + seq.(n+1) by BHSP_4:def 1;
    then
A2: ||.Partial_Sums(seq).(n+1).|| <= ||.Partial_Sums(seq).n.|| + ||.seq.(n
    +1).|| by CSSPACE:46;
    assume P[n];
    then
    ||.Partial_Sums(seq).n.|| + ||.seq.(n+1).|| <= Partial_Sums(||.seq.||)
    .n + ||.seq.(n+1).|| by XREAL_1:6;
    then
    ||.Partial_Sums(seq).(n+1).|| <= Partial_Sums(||.seq.||).n + ||.seq.(n
    +1).|| by A2,XXREAL_0:2;
    then
    ||.Partial_Sums(seq).(n+1).|| <= Partial_Sums(||.seq.||).n + ||.seq.||
    .(n+1) by CLVECT_2:def 3;
    hence P[n+1] by SERIES_1:def 1;
  end;
  Partial_Sums(||.seq.||).0 = ||.seq.||.0 by SERIES_1:def 1
    .= ||.(seq.0).|| by CLVECT_2:def 3;
  then
A3: P[0] by BHSP_4:def 1;
  thus for n holds P[n] from NAT_1:sch 1(A3,A1);
end;

theorem
  for n holds ||.Sum(seq, n).|| <= Sum(||.seq.||, n)
proof
  let n;
  ||.Partial_Sums(seq).n.|| <= Partial_Sums(||.seq.||).n by Th37;
  hence thesis by SERIES_1:def 5;
end;

theorem Th39:
  for n, m holds ||.Partial_Sums(seq).m - Partial_Sums(seq).n.||
  <= abs(Partial_Sums(||.seq.||).m - Partial_Sums(||.seq.||).n)
proof
  let n, m;
A1: now
    reconsider d = n, t = m as Integer;
    set PSseq9 = Partial_Sums(||.seq.||);
    set PSseq = Partial_Sums(seq);
    defpred P[Element of NAT] means ||.PSseq.m - PSseq.(m+$1).|| <= abs(PSseq9
    .m - PSseq9.(m+$1));
A2: PSseq9 is non-decreasing by Th35;
A3: now
      let k;
A4:   ||.seq.(m+k+1).|| >= 0 by CSSPACE:44;
A5:   abs(PSseq9.m - PSseq9.(m+(k+1))) = abs(-(PSseq9.(m+(k+1)) - PSseq9. m))
        .= abs(PSseq9.(m+k+1) - PSseq9.m) by COMPLEX1:52
        .= abs(PSseq9.(m+k) + (||.seq.||).(m+k+1) - PSseq9.m) by SERIES_1:def 1
        .= abs(||.seq.(m+k+1).|| + PSseq9.(m+k) - PSseq9.m) by CLVECT_2:def 3
        .= abs((PSseq9.(m+k) - PSseq9.m) + ||.seq.(m+k+1).||);
      ||.PSseq.m - PSseq.(m+(k+1)).|| = ||.PSseq.m - (PSseq.(m+k) + seq.(
      m+k+1)).|| by BHSP_4:def 1
        .= ||.(PSseq.m - PSseq.(m+k)) - seq.(m+k+1).|| by RLVECT_1:27
        .= ||.(PSseq.m - PSseq.(m+k)) + -seq.(m+k+1).||;
      then ||.PSseq.m - PSseq.(m+(k+1)).|| <= ||.PSseq.m - PSseq.(m+k).|| +
      ||.-seq.(m+k+1).|| by CSSPACE:46;
      then
A6:   ||.PSseq.m - PSseq.(m+(k+1)).|| <= ||.PSseq.m - PSseq.(m+k).|| +
      ||.seq.(m+k+1).|| by CSSPACE:47;
      PSseq9.(m+k) >= PSseq9.m by A2,SEQM_3:5;
      then
A7:   PSseq9.(m+k) - PSseq9.m >= 0 by XREAL_1:48;
      assume P[k];
      then ||.PSseq.m - PSseq.(m+k).|| + ||.seq.(m+k+1).|| <= abs(PSseq9.m-
      PSseq9.(m+k)) +||.seq.(m+k+1).|| by XREAL_1:6;
      then ||.PSseq.m - PSseq.(m+(k+1)).|| <= abs(-(PSseq9.(m+k) - PSseq9.m))
      + ||.seq.(m+k+1).|| by A6,XXREAL_0:2;
      then ||.PSseq.m - PSseq.(m+(k+1)).|| <= abs(PSseq9.(m+k) - PSseq9.m) +
      ||.seq.(m+k+1).|| by COMPLEX1:52;
      then ||.PSseq.m - PSseq.(m+(k+1)).|| <= (PSseq9.(m+k) - PSseq9.m) + ||.
      seq.(m+k+1).|| by A7,ABSVALUE:def 1;
      hence P[k+1] by A7,A4,A5,ABSVALUE:def 1;
    end;
    assume n >= m;
    then reconsider k = d - t as Element of NAT by INT_1:5;
A8: m + k = n;
    ||.PSseq.m - PSseq.(m+0).|| = ||.09(X).|| by RLVECT_1:15
      .= 0 by CSSPACE:42;
    then
A9: P[0] by COMPLEX1:46;
    for k holds P[k] from NAT_1:sch 1(A9,A3);
    hence thesis by A8;
  end;
  now
    reconsider d = n, t = m as Integer;
    set PSseq9 = Partial_Sums(||.seq.||);
    set PSseq = Partial_Sums(seq);
    defpred P[Element of NAT] means ||.PSseq.(n+$1) - PSseq.n.|| <= abs(PSseq9
    .(n+$1) - PSseq9.n);
A10: PSseq9 is non-decreasing by Th35;
A11: now
      let k;
A12:  abs(PSseq9.(n+(k+1)) - PSseq9.n) = abs(PSseq9.(n+k) + (||.seq.||).(
      n+k+1) - PSseq9.n) by SERIES_1:def 1
        .= abs(||.seq.(n+k+1).|| + PSseq9.(n+k) - PSseq9.n) by CLVECT_2:def 3
        .= abs(||.seq.(n+k+1).|| + (PSseq9.(n+k) - PSseq9.n));
      ||.PSseq.(n+(k+1)) - PSseq.n.|| = ||.seq.(n+k+1) + PSseq.(n+k) -
      PSseq.n.|| by BHSP_4:def 1
        .= ||.seq.(n+k+1) + (PSseq.(n+k) - PSseq.n).|| by RLVECT_1:def 3;
      then
A13:  ||.PSseq.(n+(k+1)) - PSseq.n.|| <= ||.seq.(n+k+1).|| + ||.PSseq.(n+k
      ) - PSseq.n.|| by CSSPACE:46;
      PSseq9.(n+k) >= PSseq9.n by A10,SEQM_3:5;
      then
A14:  PSseq9.(n+k) - PSseq9.n >= 0 by XREAL_1:48;
      assume P[k];
      then ||.seq.(n+k+1).|| + ||.PSseq.(n+k) - PSseq.n.|| <= ||.seq.(n+k+1)
      .|| + abs(PSseq9.(n+k)-PSseq9.n) by XREAL_1:7;
      then
      ||.PSseq.(n+(k+1)) - PSseq.n.|| <= ||.seq.(n+k+1).|| + abs(PSseq9.(
      n+k)-PSseq9.n) by A13,XXREAL_0:2;
      then
A15:  ||.PSseq.(n+(k+1)) - PSseq.n.|| <= ||.seq.(n+k+1).|| + (PSseq9.(n+k
      )-PSseq9.n) by A14,ABSVALUE:def 1;
      ||.seq.(n+k+1).|| >= 0 by CSSPACE:44;
      hence P[k+1] by A14,A15,A12,ABSVALUE:def 1;
    end;
    assume n <= m;
    then reconsider k = t - d as Element of NAT by INT_1:5;
A16: n + k = m;
    ||.PSseq.(n+0) - PSseq.n.|| = ||.09(X).|| by RLVECT_1:15
      .= 0 by CSSPACE:42;
    then
A17: P[0] by COMPLEX1:46;
    for k holds P[k] from NAT_1:sch 1(A17,A11);
    hence thesis by A16;
  end;
  hence thesis by A1;
end;

theorem Th40:
  for n,m holds ||.Sum(seq,m)-Sum(seq,n).|| <= abs( Sum(||.seq.||,
  m)-Sum(||.seq.||,n) )
proof
  let n,m;
  ||.Sum(seq, m) - Partial_Sums(seq).n.|| <= abs(Partial_Sums(||.seq.||).m
  - Partial_Sums(||.seq.||).n) by Th39;
  then
  ||.Sum(seq, m) - Sum(seq, n).|| <= abs(Sum(||.seq.||, m) - Partial_Sums(
  ||.seq.||).n) by SERIES_1:def 5;
  hence thesis by SERIES_1:def 5;
end;

theorem
  for n,m holds ||.Sum(seq,m,n).|| <= abs(Sum(||.seq.||,m,n))
proof
  let n,m;
  ||.Sum(seq,m) - Sum(seq,n).|| <= abs(Sum(||.seq.||, m) - Sum(||.seq.||,
  n)) by Th40;
  hence thesis by SERIES_1:def 6;
end;

theorem
  for X being ComplexHilbertSpace, seq being sequence of X
  holds seq is absolutely_summable implies seq is
  summable
proof
  let X be ComplexHilbertSpace, seq be sequence of X such that
A1: seq is absolutely_summable;
A2: ||.seq.|| is summable by A1,Def7;
  now
    let r;
    assume r > 0;
    then r/2 > 0;
    then consider k such that
A3: for m st m >= k holds abs(Partial_Sums(||.seq.||).m - Partial_Sums
    (||.seq.||).k) < r/2 by A2,SERIES_1:21;
    take k;
    now
      let m, n;
A4:   ||.Partial_Sums(seq).n - Partial_Sums(seq).m.|| <= abs(Partial_Sums
      (||.seq.||).n - Partial_Sums(||.seq.||).m) by Th39;
      assume m >= k & n >= k;
      then
      abs(Partial_Sums(||.seq.||).m - Partial_Sums(||.seq.||).k) < r /2 &
      abs( Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).k) < r/2 by A3;
      then
A5:   abs(Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).k) + abs(
      Partial_Sums(||.seq.||).m - Partial_Sums(||.seq.||).k) < r/2 + r/2 by
XREAL_1:8;
      abs(Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).m) = abs((
Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).k) - (Partial_Sums(||.seq
      .||).m - Partial_Sums(||.seq.||).k));
      then abs(Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).m) <= abs(
Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).k) + abs(Partial_Sums(||.
      seq.||).m - Partial_Sums(||.seq.||).k) by COMPLEX1:57;
      then abs(Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).m) < r by A5
,XXREAL_0:2;
      hence ||.Partial_Sums(seq).n - Partial_Sums(seq).m.|| < r by A4,
XXREAL_0:2;
    end;
    hence for n, m st n >= k & m >= k holds ||.Partial_Sums(seq).n -
    Partial_Sums(seq).m.|| < r;
  end;
  hence thesis by Th10;
end;

definition
  let X, seq, Cseq;
  func Cseq * seq -> sequence of X means
  :Def8:
  for n holds it.n = Cseq.n * seq.n;
  existence
  proof
    deffunc F(Element of NAT) = Cseq.$1 * seq.$1;
    thus ex M being sequence of X st for n holds M.n = F(n) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let seq1, seq2;
    assume that
A1: for n holds seq1.n = Cseq.n * seq.n and
A2: for n holds seq2.n = Cseq.n * seq.n;
    now
      let n;
      seq1.n = Cseq.n * seq.n by A1;
      hence seq1.n = seq2.n by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem
  Cseq * (seq1 + seq2) = Cseq * seq1 + Cseq * seq2
proof
  now
    let n;
    thus (Cseq * (seq1 + seq2)).n = Cseq.n * (seq1 + seq2).n by Def8
      .= Cseq.n * (seq1.n + seq2.n) by NORMSP_1:def 2
      .= Cseq.n * seq1.n + Cseq.n * seq2.n by CLVECT_1:def 2
      .= (Cseq * seq1).n + Cseq.n * seq2.n by Def8
      .= (Cseq * seq1).n + (Cseq * seq2).n by Def8
      .= (Cseq * seq1 + Cseq * seq2).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (Cseq1 + Cseq2) * seq = Cseq1 * seq + Cseq2 * seq
proof
  now
    let n;
    thus ((Cseq1 + Cseq2) * seq).n = (Cseq1 + Cseq2).n * seq.n by Def8
      .= (Cseq1.n + Cseq2.n) * seq.n by VALUED_1:1
      .= Cseq1.n * seq.n + Cseq2.n * seq.n by CLVECT_1:def 3
      .= (Cseq1 * seq).n + Cseq2.n * seq.n by Def8
      .= (Cseq1 * seq).n + (Cseq2 * seq).n by Def8
      .= (Cseq1 * seq + Cseq2 * seq).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
proof
  now
    let n;
    thus ((Cseq1 (#) Cseq2) * seq).n = (Cseq1 (#) Cseq2).n * seq.n by Def8
      .= (Cseq1.n * Cseq2.n) * seq.n by VALUED_1:5
      .= Cseq1.n * (Cseq2.n * seq.n) by CLVECT_1:def 4
      .= Cseq1.n * (Cseq2 * seq).n by Def8
      .= (Cseq1 * (Cseq2 * seq)).n by Def8;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th46:
  (z (#) Cseq) * seq = z * (Cseq * seq)
proof
  now
    let n;
    thus ((z (#) Cseq) * seq).n = (z (#) Cseq).n * seq.n by Def8
      .= (z* Cseq.n) * seq.n by VALUED_1:6
      .= z * (Cseq.n * seq.n) by CLVECT_1:def 4
      .= z * (Cseq * seq).n by Def8
      .= (z * (Cseq * seq)).n by CLVECT_1:def 14;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  Cseq * (- seq) = (- Cseq) * seq
proof
  now
    let n;
    thus (Cseq * (- seq)).n = Cseq.n * (-seq).n by Def8
      .= Cseq.n * (-(seq.n)) by BHSP_1:44
      .= (-(Cseq.n)) * seq.n by CLVECT_1:6
      .= (- Cseq).n * seq.n by VALUED_1:8
      .= ((- Cseq) * seq).n by Def8;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th48:
  Cseq is convergent & seq is convergent implies Cseq * seq is convergent
proof
  assume that
A1: Cseq is convergent and
A2: seq is convergent;
  consider p being Element of COMPLEX such that
A3: for r being Real st r > 0 ex m st for n st n >= m holds |.(Cseq.n -
  p).| < r by A1,COMSEQ_2:def 5;
  consider g such that
A4: for r st r > 0 ex m st for n st n >= m holds ||.seq.n - g.|| < r by A2,
CLVECT_2:9;
  now
    take h = p * g;
    let r;
    Cseq is bounded by A1;
    then consider b being Real such that
A5: b > 0 and
A6: for n holds |.(Cseq.n).| < b by COMSEQ_2:8;
A7: b + ||.g.|| > 0 + 0 by A5,CSSPACE:44,XREAL_1:8;
    assume
A8: r > 0;
    then consider m1 be Element of NAT such that
A9: for n st n >= m1 holds |.(Cseq.n - p).| < r/(b + ||.g.||) by A3,A7;
    consider m2 be Element of NAT such that
A10: for n st n >= m2 holds ||.seq.n - g.|| < r/(b + ||.g.||) by A4,A7,A8;
    take m = m1 + m2;
    let n such that
A11: n >= m;
    m1 + m2 >= m1 by NAT_1:12;
    then n >= m1 by A11,XXREAL_0:2;
    then ||.g.|| >= 0 & |.(Cseq.n - p).| <= r/(b + ||.g.||) by A9,CSSPACE:44;
    then
A12: ||.g.|| * |.(Cseq.n - p).| <= ||.g.|| * (r/(b + ||.g.||)) by XREAL_1:64;
A13: |.(Cseq.n).| >= 0 & ||.seq.n - g.|| >= 0 by COMPLEX1:46,CSSPACE:44;
    m >= m2 by NAT_1:12;
    then n >= m2 by A11,XXREAL_0:2;
    then
A14: ||.seq.n - g.|| < r/(b + ||.g.||) by A10;
    |.(Cseq.n).| < b by A6;
    then |.(Cseq.n).| * ||.seq.n - g.|| < b * (r/(b + ||.g.||)) by A14,A13,
XREAL_1:96;
    then
    |.(Cseq.n).| * ||.seq.n - g.|| + ||.g.|| * |.(Cseq.n - p).| < b*(r/(b
    + ||.g.||)) + ||.g.||*(r/(b + ||.g.||)) by A12,XREAL_1:8;
    then
    |.(Cseq.n).| * ||.seq.n - g.|| + ||.g.|| * |.(Cseq.n - p).| < (b*r)/(
    b + ||.g.||) + ||.g.||*(r/(b + ||.g.||)) by XCMPLX_1:74;
    then
    |.(Cseq.n).| * ||.seq.n - g.|| + ||.g.|| * |.(Cseq.n - p).| < (b*r)/(
    b + ||.g.||) + (||.g.||*r)/(b + ||.g.||) by XCMPLX_1:74;
    then |.(Cseq.n).| * ||.seq.n - g.|| + ||.g.|| * |.(Cseq.n - p).| < (b * r
    + ||.g.|| * r)/(b + ||.g.||) by XCMPLX_1:62;
    then |.(Cseq.n).| * ||.seq.n - g.|| + ||.g.|| * |.(Cseq.n - p).| < ((b +
    ||.g.||) * r)/(b + ||.g.||);
    then
A15: |.(Cseq.n).| * ||.seq.n - g.|| + ||.g.|| * |.(Cseq.n - p).| < r by A7,
XCMPLX_1:89;
    ||.(Cseq * seq).n - p * g.|| = ||.Cseq.n * seq.n - p * g.|| by Def8
      .= ||.(Cseq.n * seq.n - p * g) + 09(X).|| by RLVECT_1:4
      .= ||.(Cseq.n * seq.n - p * g) + (Cseq.n * g - Cseq.n * g).|| by
RLVECT_1:15
      .= ||.Cseq.n * seq.n - (p * g - (Cseq.n * g - Cseq.n * g)).|| by
RLVECT_1:29
      .= ||.Cseq.n * seq.n - (Cseq.n * g + (p * g - Cseq.n * g)).|| by
RLVECT_1:29
      .= ||.(Cseq.n * seq.n - Cseq.n * g) - (p * g - Cseq.n * g).|| by
RLVECT_1:27
      .= ||.(Cseq.n * seq.n - Cseq.n * g) + (Cseq.n * g - p * g).|| by
RLVECT_1:33;
    then ||.(Cseq * seq).n - p * g.|| <= ||.Cseq.n * seq.n - Cseq.n * g.|| +
    ||.Cseq.n * g - p * g.|| by CSSPACE:46;
    then
    ||.(Cseq * seq).n - p * g.|| <= ||.Cseq.n * (seq.n - g).|| + ||.Cseq.
    n * g - p * g.|| by CLVECT_1:9;
    then
    ||.(Cseq * seq).n - p * g.|| <= ||.Cseq.n * (seq.n - g).|| + ||.(Cseq
    .n - p)*g.|| by CLVECT_1:10;
    then
    ||.(Cseq * seq).n - p * g.|| <= |.(Cseq.n).| * ||.seq.n - g.|| + ||.(
    Cseq.n - p) * g.|| by CSSPACE:43;
    then
    ||.(Cseq * seq).n - p * g.|| <= |.(Cseq.n).| * ||.seq.n - g.|| + ||.g
    .|| * |.(Cseq.n - p).| by CSSPACE:43;
    hence ||.(Cseq * seq).n - h.|| < r by A15,XXREAL_0:2;
  end;
  hence thesis by CLVECT_2:9;
end;

theorem
  Cseq is bounded & seq is bounded implies Cseq * seq is bounded
proof
  assume that
A1: Cseq is bounded and
A2: seq is bounded;
  consider M1 being Real such that
A3: M1 > 0 and
A4: for n holds |.(Cseq.n).| < M1 by A1,COMSEQ_2:8;
  consider M2 be Real such that
A5: M2 > 0 and
A6: for n holds ||.seq.n.|| <= M2 by A2,CLVECT_2:def 10;
  now
    set M = M1 * M2;
    take M;
    now
      let n;
      |.(Cseq.n).| >= 0 by COMPLEX1:46;
      then
A7:   |.(Cseq.n).| * ||.seq.n.|| <= |.(Cseq.n).| * M2 by A6,XREAL_1:64;
      |.(Cseq.n).| <= M1 by A4;
      then
A8:   |.(Cseq.n).| * M2 <= M1 * M2 by A5,XREAL_1:64;
      ||.(Cseq * seq).n.|| = ||.Cseq.n * seq.n.|| by Def8
        .= |.(Cseq.n).| * ||.seq.n.|| by CSSPACE:43;
      hence ||.(Cseq * seq).n.|| <= M by A7,A8,XXREAL_0:2;
    end;
    hence M > 0 & for n holds ||.(Cseq * seq).n.|| <= M by A3,A5;
  end;
  hence thesis by CLVECT_2:def 10;
end;

theorem
  Cseq is convergent & seq is convergent implies Cseq * seq is
  convergent & lim (Cseq * seq) = lim Cseq * lim seq
proof
  assume that
A1: Cseq is convergent and
A2: seq is convergent;
  Cseq is bounded by A1;
  then consider b being Real such that
A3: b > 0 and
A4: for n holds |.(Cseq.n).| < b by COMSEQ_2:8;
A5: b + ||.lim seq.|| > 0 + 0 by A3,CSSPACE:44,XREAL_1:8;
A6: ||.lim seq.|| >= 0 by CSSPACE:44;
A7: now
    let r;
    assume r > 0;
    then
A8: r/(b + ||.lim seq.||) > 0 by A5;
    then consider m1 be Element of NAT such that
A9: for n st n >= m1 holds |.(Cseq.n - lim Cseq).| < r/(b + ||.lim
    seq.||) by A1,COMSEQ_2:def 6;
    consider m2 be Element of NAT such that
A10: for n st n >= m2 holds dist(seq.n, lim seq) < r/(b + ||.lim seq
    .||) by A2,A8,CLVECT_2:def 2;
    take m = m1 + m2;
    let n such that
A11: n >= m;
    m1 + m2 >= m1 by NAT_1:12;
    then n >= m1 by A11,XXREAL_0:2;
    then |.(Cseq.n - lim Cseq).| <= r/(b + ||.lim seq.||) by A9;
    then
A12: ||.lim seq.|| * |.(Cseq.n - lim Cseq).| <= ||.lim seq.|| * (r/(b +
    ||.lim seq.||)) by A6,XREAL_1:64;
A13: ||.seq.n - lim seq.|| >= 0 by CSSPACE:44;
    m >= m2 by NAT_1:12;
    then n >= m2 by A11,XXREAL_0:2;
    then dist(seq.n, lim seq) < r/(b + ||.lim seq.||) by A10;
    then
A14: ||.seq.n - lim seq.|| < r/(b + ||.lim seq.||) by CSSPACE:def 16;
    |.(Cseq.n).| < b & |.(Cseq.n).| >= 0 by A4,COMPLEX1:46;
    then |.(Cseq.n).| * ||.seq.n - lim seq.|| < b * (r/(b + ||.lim seq.||) )
    by A14,A13,XREAL_1:96;
    then |.(Cseq.n).|*||.seq.n-lim seq.|| + ||.lim seq.||*|.(Cseq.n-lim Cseq)
.| < b * (r/(b + ||.lim seq.||)) + ||.lim seq.|| * (r/(b + ||.lim seq.||)) by
A12,XREAL_1:8;
    then |.(Cseq.n).| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.(Cseq.n -
lim Cseq).| < (b * r)/(b + ||.lim seq.||) + ||.lim seq.|| * (r/(b + ||.lim seq
    .||)) by XCMPLX_1:74;
    then |.(Cseq.n).| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.(Cseq.n -
lim Cseq).| < (b * r)/(b + ||.lim seq.||) + (||.lim seq.|| * r)/(b + ||.lim seq
    .||) by XCMPLX_1:74;
    then |.(Cseq.n).| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.(Cseq.n -
    lim Cseq).| < (b * r + ||.lim seq.|| * r)/(b + ||.lim seq.||) by
XCMPLX_1:62;
    then |.(Cseq.n).| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.(Cseq.n -
    lim Cseq).| < ((b + ||.lim seq.||) * r)/(b + ||.lim seq.||);
    then
A15: |.(Cseq.n).| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.(Cseq.n -
    lim Cseq).| < r by A5,XCMPLX_1:89;
    ||.(Cseq * seq).n - lim Cseq * lim seq.|| = ||.Cseq.n * seq.n - lim
    Cseq * lim seq.|| by Def8
      .= ||.(Cseq.n * seq.n - lim Cseq * lim seq) + 09(X).|| by RLVECT_1:4
      .= ||.(Cseq.n * seq.n - lim Cseq * lim seq) + (Cseq.n * lim seq - Cseq
    .n * lim seq).|| by RLVECT_1:15
      .= ||.Cseq.n * seq.n - (lim Cseq * lim seq - (Cseq.n * lim seq - Cseq.
    n * lim seq)).|| by RLVECT_1:29
      .= ||.Cseq.n * seq.n - (Cseq.n * lim seq + (lim Cseq * lim seq - Cseq.
    n * lim seq)).|| by RLVECT_1:29
      .= ||.(Cseq.n * seq.n - Cseq.n * lim seq) - (lim Cseq * lim seq - Cseq
    .n * lim seq).|| by RLVECT_1:27
      .= ||.(Cseq.n * seq.n - Cseq.n * lim seq) + (Cseq.n * lim seq - lim
    Cseq * lim seq).|| by RLVECT_1:33;
    then
    ||.(Cseq * seq).n - lim Cseq * lim seq.|| <= ||.Cseq.n * seq.n - Cseq
    .n * lim seq.|| + ||.Cseq.n * lim seq - lim Cseq * lim seq.|| by CSSPACE:46
    ;
    then
    ||.(Cseq * seq).n - lim Cseq * lim seq.|| <= ||.Cseq.n * (seq.n - lim
    seq).|| + ||.Cseq.n * lim seq - lim Cseq * lim seq.|| by CLVECT_1:9;
    then
    ||.(Cseq * seq).n - lim Cseq * lim seq.|| <= ||.Cseq.n * (seq.n - lim
    seq).|| + ||.(Cseq.n - lim Cseq) * lim seq.|| by CLVECT_1:10;
    then ||.(Cseq * seq).n - lim Cseq * lim seq.|| <= |.(Cseq.n).| * ||.seq.n
    - lim seq.|| + ||.(Cseq.n - lim Cseq) * lim seq.|| by CSSPACE:43;
    then ||.(Cseq * seq).n - lim Cseq * lim seq.|| <= |.(Cseq.n).| * ||.seq.n
    - lim seq.|| + ||.lim seq.|| * |.(Cseq.n - lim Cseq).| by CSSPACE:43;
    then ||.(Cseq * seq).n - lim Cseq * lim seq.|| < r by A15,XXREAL_0:2;
    hence dist((Cseq * seq).n, (lim Cseq * lim seq)) < r by CSSPACE:def 16;
  end;
  Cseq * seq is convergent by A1,A2,Th48;
  hence thesis by A7,CLVECT_2:def 2;
end;

definition
  let Cseq;
  attr Cseq is Cauchy means
  :Def9:
  for r st r > 0 ex k st for n, m st n >= k
  & m >= k holds |.((Cseq.n - Cseq.m)).| < r;
end;

theorem
  for X being ComplexHilbertSpace, seq being sequence of X
  holds seq is Cauchy & Cseq is Cauchy implies Cseq *
  seq is Cauchy
proof
 let X be ComplexHilbertSpace, seq be sequence of X;
  assume that
A1: seq is Cauchy and
A2: Cseq is Cauchy;
  now
    let r be Real;
    assume r > 0;
    then consider k such that
A3: for n, m st n >= k & m >= k holds |.((Cseq.n - Cseq.m)).| < r by A2,Def9;
    take k;
    thus for n st n >= k holds |.((Cseq.n - Cseq.k)).| < r by A3;
  end;
  then
A4: Cseq is convergent by COMSEQ_3:46;
   seq is convergent by A1,CLVECT_2:def 11;
  hence thesis by A4,Th48,CLVECT_2:65;
end;

theorem Th52:
  for n holds Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n
  = Partial_Sums(Cseq * seq).(n+1) - (Cseq * Partial_Sums(seq)).(n+1)
proof
  defpred P[Element of NAT] means Partial_Sums((Cseq - Cseq^\1) * Partial_Sums
(seq)).$1 = Partial_Sums(Cseq * seq).($1+1) - (Cseq * Partial_Sums(seq)).($1+1)
  ;
A1: Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).0 = ((Cseq - Cseq^\1)
  * Partial_Sums(seq)).0 by BHSP_4:def 1
    .= (Cseq - Cseq^\1).0 * Partial_Sums(seq).0 by Def8
    .= (Cseq + -Cseq^\1).0 * seq.0 by BHSP_4:def 1
    .= (Cseq.0 + (-Cseq^\1).0) * seq.0 by VALUED_1:1
    .= (Cseq.0 + -(Cseq^\1).0) * seq.0 by VALUED_1:8
    .= (Cseq.0 - (Cseq^\1).0) * seq.0
    .= (Cseq.0 - Cseq.(0+1)) * seq.0 by NAT_1:def 3
    .= Cseq.0 * seq.0 - Cseq.1 * seq.0 by CLVECT_1:10;
A2: (Cseq * Partial_Sums(seq)).(0+1) = Cseq.(0+1) * Partial_Sums(seq).(0+1)
  by Def8
    .= Cseq.(0+1) * (Partial_Sums(seq).0 + seq.(0+1)) by BHSP_4:def 1
    .= Cseq.1 * (seq.0 + seq.1) by BHSP_4:def 1
    .= Cseq.1 * seq.0 + Cseq.1 * seq.1 by CLVECT_1:def 2;
A3: now
    let n;
    assume P[n];
    then Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq *
    Partial_Sums(seq)).(n+1) = Partial_Sums(Cseq * seq).(n+1) - ((Cseq *
Partial_Sums(seq)).(n+1) - (Cseq * Partial_Sums(seq)).(n+1)) by RLVECT_1:29;
    then
A4: Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq *
    Partial_Sums(seq)).(n+1) = Partial_Sums(Cseq * seq).(n+1) - 09(X) by
RLVECT_1:15;
    Partial_Sums(Cseq * seq).((n+1)+1) = Partial_Sums(Cseq * seq).(n+1) +
    (Cseq * seq).((n+1)+1) by BHSP_4:def 1
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq *
    Partial_Sums(seq)).(n+1) + (Cseq * seq).((n+1)+1) by A4,RLVECT_1:13
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + ((Cseq *
    Partial_Sums(seq)).(n+1) + (Cseq * seq).((n+1)+1)) by RLVECT_1:def 3
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq.(n+1)
    * Partial_Sums(seq).(n+1) + (Cseq * seq).((n+1)+1)) by Def8
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + ( ((Cseq.(n+
1)-Cseq.((n+1)+1))+Cseq.((n+1)+1)) *Partial_Sums(seq).(n+1) + Cseq.((n+1)+1) *
    seq.((n+1)+1) ) by Def8
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + ( ((Cseq.(n+
1) - Cseq.((n+1)+1)) * Partial_Sums(seq).(n+1) + Cseq.((n+1)+1) * Partial_Sums(
    seq).(n+1)) + Cseq.((n+1)+1) * seq.((n+1)+1)) by CLVECT_1:def 3
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (((Cseq.(n+1
) - (Cseq^\1).(n+1)) * Partial_Sums(seq).(n+1) + Cseq.((n+1)+1) * Partial_Sums(
    seq).(n+1)) + Cseq.((n+1)+1) * seq.((n+1)+1)) by NAT_1:def 3
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (((Cseq.(n+1
) + -(Cseq^\1).(n+1)) * Partial_Sums(seq).(n+1) + Cseq.((n+1)+1) * Partial_Sums
    (seq).(n+1)) + Cseq.((n+1)+1) * seq.((n+1)+1))
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (((Cseq.(n+1
) + (-Cseq^\1).(n+1)) * Partial_Sums(seq).(n+1) + Cseq.((n+1)+1) * Partial_Sums
    (seq).(n+1)) + Cseq.((n+1)+1) * seq.((n+1)+1)) by VALUED_1:8
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (((Cseq - (
Cseq^\1)).(n+1) * Partial_Sums(seq).(n+1) + Cseq.((n+1)+1) * Partial_Sums(seq).
    (n+1)) + Cseq.((n+1)+1) * seq.((n+1)+1)) by VALUED_1:1
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + ((Cseq - (
Cseq^\1)).(n+1) * Partial_Sums(seq).(n+1) + (Cseq.((n+1)+1) * Partial_Sums(seq)
    .(n+1) + Cseq.((n+1)+1) * seq.((n+1)+1))) by RLVECT_1:def 3
      .= (Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq - (
Cseq^\1)).(n+1) * Partial_Sums(seq).(n+1)) + (Cseq.((n+1)+1) * Partial_Sums(seq
    ).(n+1) + Cseq.((n+1)+1) * seq.((n+1)+1)) by RLVECT_1:def 3
      .= (Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + ((Cseq -
Cseq^\1) * Partial_Sums(seq)).(n+1)) + (Cseq.((n+1)+1) * Partial_Sums(seq).(n+1
    ) + Cseq.((n+1)+1) * seq.((n+1)+1)) by Def8
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).(n+1) + (Cseq.((
n+1)+1) * Partial_Sums(seq).(n+1) + Cseq.((n+1)+1) * seq.((n+1)+1)) by
BHSP_4:def 1
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).(n+1) + (Cseq.((
    n+1)+1) * (Partial_Sums(seq).(n+1) + seq.((n+1)+1))) by CLVECT_1:def 2
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).(n+1) + (Cseq.((
    n+1)+1) * Partial_Sums(seq).((n+1)+1)) by BHSP_4:def 1
      .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).(n+1) + (Cseq *
    Partial_Sums(seq)).((n+1)+1) by Def8;
    then Partial_Sums(Cseq * seq).((n+1)+1) - (Cseq * Partial_Sums(seq)).((n+
    1)+1) = Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).(n+1) + ((Cseq *
    Partial_Sums(seq)).((n+1)+1) - (Cseq * Partial_Sums(seq)).((n+1)+1)) by
RLVECT_1:def 3;
    then Partial_Sums(Cseq * seq).((n+1)+1) - (Cseq * Partial_Sums(seq)).((n+
    1)+1) = Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).(n+1) + 09(X)
by RLVECT_1:15;
    hence P[n+1] by RLVECT_1:4;
  end;
  Partial_Sums(Cseq * seq).(0+1) = Partial_Sums(Cseq * seq).0 + (Cseq *
  seq).(0+1) by BHSP_4:def 1
    .= (Cseq * seq).0 + (Cseq * seq).1 by BHSP_4:def 1
    .= Cseq.0 * seq.0 + (Cseq * seq).1 by Def8
    .= Cseq.0 * seq.0 + Cseq.1 * seq.1 by Def8;
  then
  Partial_Sums(Cseq * seq).(0+1) = (Cseq.0 * seq.0 + 09(X)) + Cseq.1 * seq
  .1 by RLVECT_1:4
    .= (Cseq.0 * seq.0 + (Cseq.1 * seq.0 - Cseq.1 * seq.0)) + Cseq.1 * seq.1
  by RLVECT_1:15
    .= ((Cseq.0 * seq.0 + -(Cseq.1 * seq.0)) + Cseq.1 * seq.0) + Cseq.1 *
  seq.1 by RLVECT_1:def 3
    .= Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).0 + (Cseq *
  Partial_Sums(seq)).(0+1) by A1,A2,RLVECT_1:def 3;
  then Partial_Sums(Cseq * seq).(0+1) - (Cseq * Partial_Sums(seq)).(0+1) =
  Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).0 + ((Cseq * Partial_Sums(
  seq)).(0+1) - (Cseq * Partial_Sums(seq)).(0+1)) by RLVECT_1:def 3;
  then Partial_Sums(Cseq * seq).(0+1) - (Cseq * Partial_Sums(seq)).(0+1) =
  Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).0 + 09(X) by RLVECT_1:15;
  then
A5: P[0] by RLVECT_1:4;
  thus for n holds P[n] from NAT_1:sch 1(A5,A3);
end;

theorem Th53:
  for n holds Partial_Sums(Cseq * seq).(n+1) = (Cseq *
Partial_Sums(seq)).(n+1) - Partial_Sums((Cseq^\1 - Cseq) * Partial_Sums(seq)).n
proof
  let n;
  Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq *
  Partial_Sums(seq)).(n+1) = (Partial_Sums(Cseq * seq).(n+1) - (Cseq *
  Partial_Sums(seq)).(n+1)) + (Cseq * Partial_Sums(seq)).(n+1) by Th52;
  then Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq *
  Partial_Sums(seq)).(n+1) = Partial_Sums(Cseq * seq).(n+1) - ((Cseq *
  Partial_Sums(seq)).(n+1) - (Cseq * Partial_Sums(seq)).(n+1)) by RLVECT_1:29;
  then Partial_Sums((Cseq - Cseq^\1) * Partial_Sums(seq)).n + (Cseq *
  Partial_Sums(seq)).(n+1) = Partial_Sums(Cseq * seq).(n+1) - 09(X) by
RLVECT_1:15;
  then Partial_Sums(Cseq * seq).(n+1) = (Cseq * Partial_Sums(seq)).(n+1) +
  Partial_Sums((Cseq + -(Cseq^\1))*Partial_Sums(seq)).n by RLVECT_1:13;
  then Partial_Sums(Cseq * seq).(n+1) = (Cseq * Partial_Sums(seq)).(n+1) +
  Partial_Sums(((-1r) (#) (Cseq^\1) - -Cseq) * Partial_Sums(seq)).n by
COMSEQ_1:11;
  then Partial_Sums(Cseq * seq).(n+1) = (Cseq * Partial_Sums(seq)).(n+1) +
  Partial_Sums(((-1r) (#) (Cseq^\1) - (-1r) (#) Cseq) * Partial_Sums(seq)).n
by COMSEQ_1:11;
  then Partial_Sums(Cseq * seq).(n+1) = (Cseq * Partial_Sums(seq)).(n+1) +
  Partial_Sums(((-1r) (#) (Cseq^\1 - Cseq)) * Partial_Sums(seq)).n by
COMSEQ_1:18;
  then Partial_Sums(Cseq * seq).(n+1) = (Cseq * Partial_Sums(seq)).(n+1) +
  Partial_Sums((-1r) * ((Cseq^\1 - Cseq) * Partial_Sums(seq))).n by Th46;
  then
  Partial_Sums(Cseq * seq).(n+1) = (Cseq * Partial_Sums(seq)).(n+1) + ((-
  1r) * Partial_Sums((Cseq^\1 - Cseq) * Partial_Sums(seq))).n by Th3;
  then Partial_Sums(Cseq * seq).(n+1) = (Cseq * Partial_Sums(seq)).(n+1) + (-
  1r) * Partial_Sums((Cseq^\1 - Cseq) * Partial_Sums(seq)).n by CLVECT_1:def 14
;
  hence thesis by CLVECT_1:3;
end;

theorem
  for n holds Sum(Cseq*seq,n+1) = (Cseq*Partial_Sums(seq)).(n+1) - Sum((
  Cseq^\1 - Cseq)*Partial_Sums(seq),n) by Th53;