The Mizar article:

Introduction to Banach and Hilbert Spaces --- Part III

by
Jan Popiolek

Received July 19, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: BHSP_3
[ MML identifier index ]


environ

 vocabulary BHSP_1, PRE_TOPC, NORMSP_1, ORDINAL2, SEQM_3, SEQ_1, RLVECT_1,
      METRIC_1, FUNCT_1, ARYTM_1, ARYTM_3, ABSVALUE, RELAT_1, SEQ_2, LATTICES,
      BHSP_3, ARYTM;
 notation TARSKI, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1,
      FUNCT_2, SEQ_1, SEQM_3, ABSVALUE, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_1,
      BHSP_1, BHSP_2;
 constructors REAL_1, NAT_1, SEQ_1, ABSVALUE, BHSP_2, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, SEQM_3, STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, MEMBERED,
      ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems REAL_1, NAT_1, REAL_2, AXIOMS, FUNCT_1, SEQ_2, SEQM_3, SEQ_4,
      FUNCT_2, ABSVALUE, RLVECT_1, BHSP_1, BHSP_2, NORMSP_1, RELAT_1, RELSET_1,
      XREAL_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes NAT_1, SEQ_1, BHSP_1;

begin

 reserve X for RealUnitarySpace,
         x, g, g1, h for Point of X,
         a, p, r, M, M1, M2 for Real,
         seq, seq1, seq2, seq3 for sequence of X,
         Nseq,Nseq1,Nseq2 for increasing Seq_of_Nat,
         Rseq for Real_Sequence,
         k, l, l1, l2, l3, n, m, m1, m2 for Nat;

deffunc 0'(RealUnitarySpace) = 0.$1;

definition
          let X;
          let seq;
          attr seq is Cauchy means
:Def1:    for r st r > 0 ex k st for n, m st ( n >= k & m >= k )
          holds dist((seq.n), (seq.m)) < r;
  synonym seq is_Cauchy_sequence;
end;

theorem
    seq is constant implies seq is_Cauchy_sequence
proof
     assume
A1:     seq is constant;
     let r such that
A2:   r > 0;
     take k = 0;
     let n, m such that
       n >= k & m >= k;
       dist((seq.n), (seq.m)) = dist((seq.n), (seq.n)) by A1,BHSP_1:70
                            .= 0 by BHSP_1:41;
     hence dist((seq.n), (seq.m)) < r by A2;
  end;

theorem
    seq is_Cauchy_sequence iff for r st r > 0 ex k st for n, m st
    ( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r
proof
     thus
       seq is_Cauchy_sequence implies for r st r > 0 ex k st for n, m st
     ( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r
     proof
          assume
A1:          seq is_Cauchy_sequence;
          let r; assume r > 0;
          then consider l such that
     A2:   for n, m st ( n >= l & m >= l ) holds
          dist((seq.n), (seq.m)) < r by A1,Def1;
          take k = l;
          let n, m; assume n >= k & m >= k;
          then dist((seq.n), (seq.m)) < r by A2;
          hence thesis by BHSP_1:def 5;
          end;
       ( for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds
     ||.(seq.n) - (seq.m).|| < r ) implies seq is_Cauchy_sequence
     proof
          assume
     A3:   for r st r > 0 ex k st for n, m st ( n >= k & m >= k )
          holds ||.(seq.n) - (seq.m).|| < r;
          let r; assume r > 0;
          then consider l such that
     A4:   for n, m st ( n >= l & m >= l ) holds
          ||.(seq.n) - (seq.m).|| < r by A3;
          take k = l;
          let n, m; assume n >= k & m >= k;
          then ||.(seq.n) - (seq.m).|| < r by A4;
          hence dist((seq.n), (seq.m)) < r by BHSP_1:def 5;
     end;
     hence thesis;
end;

theorem
    seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies
    seq1 + seq2 is_Cauchy_sequence
proof
     assume that
 A1:  seq1 is_Cauchy_sequence and
 A2:  seq2 is_Cauchy_sequence;
      let r; assume r > 0;
 then A3:  r/2 > 0 by SEQ_2:3;
      then consider m1 such that
 A4:  for n, m st ( n >= m1 & m >= m1 ) holds
      dist((seq1.n), (seq1.m)) < r/2 by A1,Def1;
      consider m2 such that
 A5:  for n, m st ( n >= m2 & m >= m2 ) holds
      dist((seq2.n), (seq2.m)) < r/2 by A2,A3,Def1;
      take k = m1 + m2;
      let n, m such that
  A6:  n >= k & m >= k;
        m1 + m2 >= m1 by NAT_1:37;
      then n >= m1 & m >= m1 by A6,AXIOMS:22;
  then A7:  dist((seq1.n), (seq1.m)) < r/2 by A4;
        k >= m2 by NAT_1:37;
      then n >= m2 & m >= m2 by A6,AXIOMS:22;
      then dist((seq2.n), (seq2.m)) < r/2 by A5;
      then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2
      by A7,REAL_1:67;
  then A8:  dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r
      by XCMPLX_1:66;
        dist((seq1 + seq2).n, (seq1 + seq2).m)
    = dist((seq1.n) + (seq2.n), (seq1 + seq2).m) by NORMSP_1:def 5
   .= dist((seq1.n) + (seq2.n), (seq1.m) + (seq2.m)) by NORMSP_1:def 5;
      then dist((seq1 + seq2).n, (seq1 + seq2).m) <=
      dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) by BHSP_1:47;
      hence dist((seq1 + seq2).n, (seq1 + seq2).m) < r by A8,AXIOMS:22;
  end;

theorem
    seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies
    seq1 - seq2 is_Cauchy_sequence
proof
     assume that
 A1:  seq1 is_Cauchy_sequence and
 A2:  seq2 is_Cauchy_sequence;
      let r; assume r > 0;
 then A3:  r/2 > 0 by SEQ_2:3;
      then consider m1 such that
 A4:  for n, m st ( n >= m1 & m >= m1 ) holds
      dist((seq1.n), (seq1.m)) < r/2 by A1,Def1;
      consider m2 such that
 A5:  for n, m st ( n >= m2 & m >= m2 ) holds
      dist((seq2.n), (seq2.m)) < r/2 by A2,A3,Def1;
      take k = m1 + m2;
      let n, m such that
  A6:  n >= k & m >= k;
        m1 + m2 >= m1 by NAT_1:37;
      then n >= m1 & m >= m1 by A6,AXIOMS:22;
  then A7:  dist((seq1.n), (seq1.m)) < r/2 by A4;
        k >= m2 by NAT_1:37;
      then n >= m2 & m >= m2 by A6,AXIOMS:22;
      then dist((seq2.n), (seq2.m)) < r/2 by A5;
      then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2
      by A7,REAL_1:67;
  then A8:  dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r
      by XCMPLX_1:66;
        dist((seq1 - seq2).n, (seq1 - seq2).m)
    = dist((seq1.n) - (seq2.n), (seq1 - seq2).m) by NORMSP_1:def 6
   .= dist((seq1.n) - (seq2.n), (seq1.m) - (seq2.m)) by NORMSP_1:def 6;
      then dist((seq1 - seq2).n, (seq1 - seq2).m) <=
      dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) by BHSP_1:48;
      hence dist((seq1 - seq2).n, (seq1 - seq2).m) < r by A8,AXIOMS:22;
  end;

theorem Th5:
  seq is_Cauchy_sequence implies a * seq is_Cauchy_sequence
proof
     assume
A1:         seq is_Cauchy_sequence;
     A2:    now assume
     A3:   a = 0;
           let r; assume r > 0;
           then consider m1 such that
     A4:   for n, m st ( n >= m1 & m >= m1 ) holds
           dist((seq.n), (seq.m)) < r by A1,Def1;
           take k = m1;
           let n, m; assume n >= k & m >= k;
     then A5:   dist((seq.n), (seq.m)) < r by A4;
          dist(a * (seq.n), a * (seq.m))
         = dist(0'(X), 0 * (seq.m)) by A3,RLVECT_1:23
        .= dist(0'(X), 0'(X)) by RLVECT_1:23
        .= 0 by BHSP_1:41;
           then dist(a * (seq.n), a * (seq.m)) < r by A5,BHSP_1:44;
           then dist((a * seq).n, a * (seq.m)) < r by NORMSP_1:def 8;
           hence dist((a * seq).n, (a * seq).m) < r by NORMSP_1:def 8;
           end;
             now assume
A6:        a <> 0;
     then A7:   abs(a) > 0 by ABSVALUE:6;
           let r such that
     A8:   r > 0;
     A9:   abs(a) <> 0 by A6,ABSVALUE:6;
             0/abs(a) = 0;
           then r/abs(a) > 0 by A7,A8,REAL_1:73;
           then consider m1 such that
     A10:   for n, m st ( n >= m1 & m >= m1 ) holds
           dist((seq.n), (seq.m)) < r/abs(a) by A1,Def1;
           take k = m1;
           let n, m; assume n >= k & m >= k;
     then A11:   dist((seq.n), (seq.m)) < r/abs(a) by A10;
     A12:   dist(a * (seq.n), a * (seq.m))
         = ||.(a * (seq.n)) - (a * (seq.m)).|| by BHSP_1:def 5
        .= ||.a * ((seq.n) - (seq.m)).|| by RLVECT_1:48
        .= abs(a) * ||.(seq.n) - (seq.m).|| by BHSP_1:33
        .= abs(a) * dist((seq.n), (seq.m)) by BHSP_1:def 5;
             abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9
                            .= abs(a) *abs(a)" * r by XCMPLX_1:4
                            .= 1 * r by A9,XCMPLX_0:def 7
                            .= r;
           then dist((a * (seq.n)), (a * (seq.m))) < r
           by A7,A11,A12,REAL_1:70;
           then dist((a * seq).n, (a * (seq.m))) < r by NORMSP_1:def 8;
           hence dist((a * seq).n, (a * seq).m) < r by NORMSP_1:def 8;
           end;
     hence thesis by A2,Def1;
end;

theorem
    seq is_Cauchy_sequence implies - seq is_Cauchy_sequence
proof
     assume seq is_Cauchy_sequence;
     then (-1) * seq is_Cauchy_sequence by Th5;
     hence thesis by BHSP_1:77;
end;

theorem Th7:
  seq is_Cauchy_sequence implies seq + x is_Cauchy_sequence
proof
     assume
A1:         seq is_Cauchy_sequence;
           let r; assume r > 0;
           then consider m1 such that
     A2:    for n, m st ( n >= m1 & m >= m1 ) holds
           dist((seq.n), (seq.m)) < r by A1,Def1;
           take k = m1;
           let n, m; assume n >= k & m >= k;
     then A3:    dist((seq.n), (seq.m)) < r by A2;
             dist((seq.n) + x, (seq.m) + x) <= dist((seq.n), (seq.m)) +
           dist(x, x) by BHSP_1:47;
           then dist((seq.n) + x, (seq.m) + x) <=
           dist((seq.n), (seq.m)) + 0 by BHSP_1:41;
           then dist((seq.n) + x, (seq.m) + x) < r by A3,AXIOMS:22;
           then dist((seq + x).n, (seq.m) + x) < r by BHSP_1:def 12;
           hence dist((seq + x).n, (seq + x).m) < r by BHSP_1:def 12;
end;

theorem
    seq is_Cauchy_sequence implies seq - x is_Cauchy_sequence
proof
     assume seq is_Cauchy_sequence;
     then seq + (-x) is_Cauchy_sequence by Th7;
     hence thesis by BHSP_1:78;
end;

theorem
    seq is convergent implies seq is_Cauchy_sequence
proof
     assume seq is convergent;
     then consider h such that
A1:   for r st r > 0 ex k st for n st n >= k holds
     dist((seq.n), h) < r by BHSP_2:def 1;
     let r; assume r > 0;
     then r/2 > 0 by SEQ_2:3;
     then consider m1 such that
A2:   for n st n >= m1 holds dist((seq.n), h) < r/2 by A1;
     take k = m1;
     let n, m; assume
A3:   n >= k & m >= k;
then A4:   dist((seq.n), h) < r/2 by A2;
     A5: dist((seq.m), h) < r/2 by A2,A3;
A6:   dist((seq.n), (seq.m)) <= dist((seq.n), h) + dist(h, (seq.m))
     by BHSP_1:42;
       dist((seq.n), h) + dist(h, (seq.m)) < r/2 + r/2
     by A4,A5,REAL_1:67;
     then dist((seq.n), h) + dist(h, (seq.m)) < r by XCMPLX_1:66;
     hence dist((seq.n), (seq.m)) < r by A6,AXIOMS:22;
end;

definition
          let X;
          let seq1, seq2;
          pred seq1 is_compared_to seq2 means
:Def2:    for r st r > 0 ex m st for n st n >= m holds
          dist(seq1.n, seq2.n) < r;
end;

theorem
Th10:  seq is_compared_to seq
proof
     let r such that
A1:   r > 0;
     take m = 0;
     let n such that
       n >= m;
     thus dist((seq.n), (seq.n)) < r by A1,BHSP_1:41;
  end;

theorem
Th11:  seq1 is_compared_to seq2 implies seq2 is_compared_to seq1
proof
     assume
A1:     seq1 is_compared_to seq2;
     let r; assume r > 0;
     then consider k such that
A2:   for n st n >= k holds
     dist((seq1.n), (seq2.n)) < r by A1,Def2;
     take m = k;
     let n; assume n >= m;
     hence thesis by A2;
end;

definition let X; let seq1, seq2;
  redefine pred seq1 is_compared_to seq2;
  reflexivity by Th10;
  symmetry by Th11;
end;

theorem
    seq1 is_compared_to seq2 & seq2 is_compared_to seq3
    implies seq1 is_compared_to seq3
proof
     assume that
A1:  seq1 is_compared_to seq2 and
A2:  seq2 is_compared_to seq3;
     let r; assume r > 0;
then A3:  r/2 > 0 by SEQ_2:3;
     then consider m1 such that
A4:  for n st n >= m1 holds
     dist((seq1.n), (seq2.n)) < r/2 by A1,Def2;
     consider m2 such that
A5:  for n st n >= m2 holds
     dist((seq2.n), (seq3.n)) < r/2 by A2,A3,Def2;
     take m = m1 + m2;
     let n such that
A6:   n >= m;
       m1 + m2 >= m1 by NAT_1:37;
     then n >= m1 by A6,AXIOMS:22;
then A7:   dist((seq1.n), (seq2.n)) < r/2 by A4;
       m >= m2 by NAT_1:37;
     then n >= m2 by A6,AXIOMS:22;
     then dist((seq2.n), (seq3.n)) < r/2 by A5;
     then dist((seq1.n), (seq2.n)) + dist((seq2.n), (seq3.n)) < r/2 + r/2
     by A7,REAL_1:67;
then A8:   dist((seq1.n), (seq2.n)) + dist((seq2.n), (seq3.n)) < r
     by XCMPLX_1:66;
       dist((seq1.n), (seq3.n)) <=
     dist((seq1.n), (seq2.n)) + dist((seq2.n), (seq3.n))
     by BHSP_1:42;
     hence dist((seq1.n), (seq3.n)) < r by A8,AXIOMS:22;
end;

theorem
    seq1 is_compared_to seq2 iff for r st r > 0 ex m st
    for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r
proof
     thus
       seq1 is_compared_to seq2 implies for r st r > 0 ex m st
     for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r
     proof
          assume
A1:          seq1 is_compared_to seq2;
          let r; assume r > 0;
          then consider m1 such that
     A2:   for n st n >= m1 holds
          dist((seq1.n), (seq2.n)) < r by A1,Def2;
          take m = m1;
          let n; assume n >= m;
          then dist((seq1.n), (seq2.n)) < r by A2;
          hence thesis by BHSP_1:def 5;
          end;
       ( for r st r > 0 ex m st for n st n >= m holds
     ||.(seq1.n) - (seq2.n).|| < r ) implies seq1 is_compared_to seq2
     proof
          assume
     A3:   for r st r > 0 ex m st for n st n >= m holds
          ||.(seq1.n) - (seq2.n).|| < r;
          let r; assume r > 0;
          then consider m1 such that
     A4:   for n st n >= m1 holds
          ||.(seq1.n) - (seq2.n).|| < r by A3;
          take m = m1;
          let n; assume n >= m;
          then ||.(seq1.n) - (seq2.n).|| < r by A4;
          hence thesis by BHSP_1:def 5;
          end;
     hence thesis;
end;

theorem
    ( ex k st for n st n >= k holds seq1.n = seq2.n )
    implies seq1 is_compared_to seq2
proof
     assume
A1:   ex k st for n st n >= k holds seq1.n = seq2.n;
     let r such that
A2:   r > 0;
     consider m such that
A3:   for n st n >= m holds seq1.n = seq2.n by A1;
     take k = m;
     let n; assume n >= k;
     then dist((seq1.n), (seq2.n)) = dist((seq1.n), (seq1.n)) by A3
                              .= 0 by BHSP_1:41;
     hence dist((seq1.n), (seq2.n)) < r by A2;
end;

theorem
    seq1 is_Cauchy_sequence & seq1 is_compared_to seq2
     implies seq2 is_Cauchy_sequence
proof
     assume that
A1:   seq1 is_Cauchy_sequence and
A2:   seq1 is_compared_to seq2;
     let r; assume r > 0;
then A3:   r/3 > 0 by SEQ_4:4;
     then consider m1 such that
A4:   for n, m st ( n >= m1 & m >= m1 ) holds
     dist((seq1.n), (seq1.m)) < r/3 by A1,Def1;
     consider m2 such that
A5:   for n st n >= m2 holds
     dist((seq1.n), (seq2.n)) < r/3 by A2,A3,Def2;
     take k = m1 + m2;
     let n, m such that
A6:   n >= k & m >= k;
       m1 + m2 >= m1 by NAT_1:37;
     then n >= m1 & m >= m1 by A6,AXIOMS:22;
then A7:   dist((seq1.n), (seq1.m)) < r/3 by A4;
     A8:   k >= m2 by NAT_1:37;
     then n >= m2 by A6,AXIOMS:22;
     then A9: dist((seq1.n), (seq2.n)) < r/3 by A5;
       m >= m2 by A6,A8,AXIOMS:22;
then A10:   dist((seq1.m), (seq2.m)) < r/3 by A5;
A11:   dist((seq2.n), (seq1.n)) + dist((seq1.n), (seq1.m)) < r/3 + r/3
     by A7,A9,REAL_1:67;
       dist((seq2.n), (seq1.m)) <=
     dist((seq2.n), (seq1.n)) + dist((seq1.n), (seq1.m))
     by BHSP_1:42;
     then dist((seq2.n), (seq1.m)) < r/3 + r/3 by A11,AXIOMS:22;
     then dist((seq2.n), (seq1.m)) + dist((seq1.m), (seq2.m)) <
     r/3 + r/3 + r/3 by A10,REAL_1:67;
then A12:   dist((seq2.n), (seq1.m)) + dist((seq1.m), (seq2.m)) < r by XCMPLX_1
:69;
       dist((seq2.n), (seq2.m)) <= dist((seq2.n), (seq1.m)) +
     dist((seq1.m), (seq2.m)) by BHSP_1:42;
     hence dist((seq2.n), (seq2.m)) < r by A12,AXIOMS:22;
end;

theorem
    seq1 is convergent & seq1 is_compared_to seq2
    implies seq2 is convergent
proof
     assume that
A1:   seq1 is convergent and
A2:   seq1 is_compared_to seq2;
       now let r; assume r > 0;
then A3:   r/2 > 0 by SEQ_2:3;
     then consider m1 such that
A4:   for n st n >= m1 holds
     dist((seq1.n), (lim seq1)) < r/2 by A1,BHSP_2:def 2;
     consider m2 such that
A5:   for n st n >= m2 holds
     dist((seq1.n), (seq2.n)) < r/2 by A2,A3,Def2;
     take m = m1 + m2;
     let n such that
A6:   n >= m;
       m1 + m2 >= m1 by NAT_1:37;
     then n >= m1 by A6,AXIOMS:22;
then A7:   dist((seq1.n), (lim seq1)) < r/2 by A4;
       m >= m2 by NAT_1:37;
     then n >= m2 by A6,AXIOMS:22;
     then dist((seq1.n), (seq2.n)) < r/2 by A5;
     then dist((seq2.n), (seq1.n)) + dist((seq1.n), (lim seq1)) <
     r/2 + r/2 by A7,REAL_1:67;
then A8:   dist((seq2.n), (seq1.n)) + dist((seq1.n), (lim seq1)) < r
     by XCMPLX_1:66;
       dist((seq2.n), (lim seq1)) <=
     dist((seq2.n), (seq1.n)) + dist((seq1.n), (lim seq1))
     by BHSP_1:42;
     hence dist((seq2.n), (lim seq1)) < r by A8,AXIOMS:22;
     end;
     hence thesis by BHSP_2:def 1;
end;

theorem
    seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2
    implies seq2 is convergent & lim seq2 = g
proof
     assume that
A1:  seq1 is convergent and
A2:  lim seq1 = g and
A3:   seq1 is_compared_to seq2;
A4:   now let r; assume r > 0;
then A5:   r/2 > 0 by SEQ_2:3;
     then consider m1 such that
A6:   for n st n >= m1 holds
     dist((seq1.n), g) < r/2 by A1,A2,BHSP_2:def 2;
     consider m2 such that
A7:   for n st n >= m2 holds
     dist((seq1.n), (seq2.n)) < r/2 by A3,A5,Def2;
     take m = m1 + m2;
     let n such that
A8:   n >= m;
       m1 + m2 >= m1 by NAT_1:37;
     then n >= m1 by A8,AXIOMS:22;
then A9:   dist((seq1.n), g) < r/2 by A6;
       m >= m2 by NAT_1:37;
     then n >= m2 by A8,AXIOMS:22;
     then dist((seq1.n), (seq2.n)) < r/2 by A7;
     then dist((seq2.n), (seq1.n)) + dist((seq1.n), g) <
     r/2 + r/2 by A9,REAL_1:67;
then A10:   dist((seq2.n), (seq1.n)) + dist((seq1.n), g) < r by XCMPLX_1:66;
       dist((seq2.n), g) <=
     dist((seq2.n), (seq1.n)) + dist((seq1.n), g)
     by BHSP_1:42;
     hence dist((seq2.n), g) < r by A10,AXIOMS:22;
     end;
     then seq2 is convergent by BHSP_2:def 1;
     hence thesis by A4,BHSP_2:def 2;
end;

definition
          let X;
          let seq;
          attr seq is bounded means
:Def3:   ex M st M > 0 & for n holds ||.seq.n.|| <= M;
end;

theorem Th18:
  seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded
proof
     assume that
A1:  seq1 is bounded and
A2:  seq2 is bounded;
     consider M1 such that
A3:  M1 > 0 and
A4:  for n holds ||.seq1.n.|| <= M1 by A1,Def3;
     consider M2 such that
A5:  M2 > 0 and
A6:  for n holds ||.seq2.n.|| <= M2 by A2,Def3;
A7:   M1 + M2 > 0 + 0 by A3,A5,REAL_1:67;
       now let n;
A8:  ||.seq1.n.|| <= M1 by A4;
       ||.seq2.n.|| <= M2 by A6;
then A9:   ||.seq1.n.|| + ||.seq2.n.|| <= M1 + M2 by A8,REAL_1:55;
       ||.(seq1 + seq2).n.|| = ||.seq1.n + seq2.n.|| by NORMSP_1:def 5;
     then ||.(seq1 + seq2).n.|| <= ||.seq1.n.|| + ||.seq2.n.|| by BHSP_1:36;
     hence ||.(seq1 + seq2).n.|| <= M1 + M2 by A9,AXIOMS:22;
     end;
     hence thesis by A7,Def3;
end;

theorem Th19:
  seq is bounded implies -seq is bounded
proof
     assume seq is bounded;
    then consider M such that
A1:  M > 0 and
A2:  for n holds ||.seq.n.|| <= M by Def3;
      now let n;
      ||.(- seq).n.|| = ||.- (seq.n).|| by BHSP_1:def 10
                 .= ||.seq.n.|| by BHSP_1:37;
    hence ||.(- seq).n.|| <= M by A2;
    end;
    hence thesis by A1,Def3;
end;

theorem
    seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded
proof
     assume that
A1:   seq1 is bounded and
A2:   seq2 is bounded;
A3:   - seq2 is bounded by A2,Th19;
       seq1 - seq2 = seq1 + (- seq2) by BHSP_1:71;
     hence thesis by A1,A3,Th18;
end;

theorem
    seq is bounded implies a * seq is bounded
proof
     assume seq is bounded;
    then consider M such that
A1:  M > 0 and
A2:  for n holds ||.seq.n.|| <= M by Def3;
A3:  a = 0 implies a * seq is bounded
    proof
    assume
A4: a = 0;
      now let n;
      ||.(a * seq).n.|| = ||.0 * (seq.n).|| by A4,NORMSP_1:def 8
                   .= ||.0'(X).|| by RLVECT_1:23
                   .= 0 by BHSP_1:32;
    hence ||.(a * seq).n.|| <= M by A1;
    end;
    hence thesis by A1,Def3;
    end;
      a <> 0 implies a * seq is bounded
    proof
    assume a <> 0;
    then abs(a) > 0 by ABSVALUE:6;
then A5:  abs(a) * M > 0 by A1,REAL_2:122;
      now let n;
A6:  ||.seq.n.|| <= M by A2;
A7:  ||.(a * seq).n.|| = ||.a * (seq.n).|| by NORMSP_1:def 8
                   .= abs(a) * ||.seq.n.|| by BHSP_1:33;
      abs(a) >= 0 by ABSVALUE:5;
    hence ||.(a * seq).n.|| <= abs(a) * M by A6,A7,AXIOMS:25;
    end;
    hence thesis by A5,Def3;
    end;
    hence thesis by A3;
end;

theorem
    seq is constant implies seq is bounded
proof
     assume
       seq is constant;
     then consider x such that
A1:   for n holds seq.n = x by NORMSP_1:def 4;
A2:   x = 0'(X) implies seq is bounded
     proof
     assume
A3:  x = 0'(X);
     consider M being real number such that
A4:  M > 0 by REAL_1:76;
     reconsider M as Real by XREAL_0:def 1;
       now let n;
       seq.n = 0'(X) by A1,A3;
     hence ||.seq.n.|| <= M by A4,BHSP_1:32;
     end;
     hence thesis by A4,Def3;
     end;
       x <> 0'(X) implies seq is bounded
     proof
     assume x <> 0'(X);
     then A5: ||.x.|| >= 0 & ||.x.|| <> 0 by BHSP_1:32,34;
     consider M being real number such that
A6:  ||.x.|| < M by REAL_1:76;
     reconsider M as Real by XREAL_0:def 1;
       for n holds ||.seq.n.|| <= M by A1,A6;
     hence thesis by A5,A6,Def3;
     end;
     hence thesis by A2;
end;

theorem Th23:
  for m ex M st ( M > 0 & for n st n <= m holds ||.seq.n.|| < M )
proof
   defpred _P[Nat] means
   ex M st ( M > 0 & for n st n <= $1 holds ||.seq.n.|| < M );
A1: _P[0] proof take M = ||.(seq.0).|| + 1;
       ||.(seq.0).|| >= 0 by BHSP_1:34;
     then ||.(seq.0).|| + 1 > 0 + 0 by REAL_1:67;
     hence M > 0;
     let n such that
A2:   n <= 0;
      n = 0 by A2,NAT_1:18;
     then ||.seq.n.|| + 0 < M by REAL_1:67;
     hence ||.seq.n.|| < M;
     end;
A3:  for m st _P[m] holds _P[m+1] proof let m;
     given M1 such that
A4:   M1 > 0 and
A5:   for n st n <= m holds ||.seq.n.|| < M1;
A6:   now assume
A7:   ||.seq.(m+1).|| <= M1;
     take M = M1 + 1;
       M1 + 1 > 0 + 0 by A4,REAL_1:67;
     hence M > 0;
     let n such that
A8:   n <= m + 1;
A9:   now assume m >= n;
then A10:   ||.seq.n.|| < M1 by A5;
       M > M1 + 0 by REAL_1:67;
     hence ||.seq.n.|| < M by A10,AXIOMS:22;
     end;
       now assume A11: n = m + 1;
       M > M1 + 0 by REAL_1:67;
     hence ||.seq.n.|| < M by A7,A11,AXIOMS:22;
     end;
     hence ||.seq.n.|| < M by A8,A9,NAT_1:26;
     end;
       now assume
A12:   ||.seq.(m+1).|| >= M1;
     take M = ||.seq.(m+1).|| + 1;
       ||.seq.(m+1).|| >= 0 by BHSP_1:34;
     then M > 0 + 0 by REAL_1:67;
     hence M > 0;
     let n such that
A13:   n <= m + 1;
A14:   now assume m >= n;
     then ||.seq.n.|| < M1 by A5;
     then ||.seq.n.|| < ||.seq.(m+1).|| by A12,AXIOMS:22;
     then ||.seq.n.|| + 0 < M by REAL_1:67;
     hence ||.seq.n.|| < M;
     end;
       now assume n = m + 1;
     then ||.seq.n.|| + 0 < M by REAL_1:67;
     hence ||.seq.n.|| < M;
     end;
     hence ||.seq.n.|| < M by A13,A14,NAT_1:26;
     end;
     hence ex M st ( M > 0 & for n st n <= m + 1 holds ||.seq.n.|| < M )
     by A6;
     end;
     thus for m holds _P[m] from Ind(A1,A3);
end;

theorem Th24:
  seq is convergent implies seq is bounded
proof
     assume seq is convergent;
     then consider g such that
A1:   for r st r > 0 ex m st for n st n >= m
     holds ||.seq.n - g.|| < r by BHSP_2:9;
     consider m1 such that
A2:   for n st n >= m1 holds
     ||.seq.n - g.|| < 1 by A1;
A3:   now take p = ||.g.|| + 1;
       ||.g.|| >= 0 by BHSP_1:34;
     then 0 + 0 < p by REAL_1:67;
     hence p > 0;
     let n; assume n >= m1;
then A4:   ||.seq.n - g.|| < 1 by A2;
       ||.seq.n.|| - ||.g.|| <= ||.seq.n - g.|| by BHSP_1:38;
     then ||.seq.n.|| - ||.g.|| < 1 by A4,AXIOMS:22;
     hence ||.seq.n.|| < p by REAL_1:84;
     end;
       now consider M1 such that
A5:   M1 > 0 and
A6:   for n st n >= m1 holds ||.seq.n.|| < M1 by A3;
     consider M2 such that
A7:   M2 > 0 and
A8:   for n st n <= m1 holds ||.seq.n.|| < M2 by Th23;
     take M = M1 + M2;
       M > 0 + 0 by A5,A7,REAL_1:67;
     hence M > 0;
     A9: M > M1 + 0 by A7,REAL_1:67;
     A10: M > 0 + M2 by A5,REAL_1:67;
     let n;
A11:   now assume n >= m1;
     then ||.seq.n.|| < M1 by A6;
     hence ||.seq.n.|| <= M by A9,AXIOMS:22;
     end;
       now assume n <= m1;
     then ||.seq.n.|| < M2 by A8;
     hence ||.seq.n.|| <= M by A10,AXIOMS:22;
     end;
     hence ||.seq.n.|| <= M by A11;
     end;
     hence thesis by Def3;
  end;

theorem
    seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded
proof
     assume that
A1:   seq1 is bounded and
A2:   seq1 is_compared_to seq2;
     consider p such that
A3:   p > 0 and
A4:   for n holds ||.seq1.n.|| <= p by A1,Def3;
     consider m1 such that
A5:   for n st n >= m1 holds
     dist((seq1.n), (seq2.n)) < 1 by A2,Def2;
A6:     p + 1 > 0 + 0 by A3,REAL_1:67;
A7:   ex M st ( M > 0 & for n st n >= m1 holds ||.seq2.n.|| < M )
     proof
     take M = p + 1;
       now let n; assume n >= m1;
     then dist((seq1.n), (seq2.n)) < 1 by A5;
then A8:   ||.seq2.n - seq1.n.|| < 1 by BHSP_1:def 5;
       ||.seq2.n.|| - ||.seq1.n.|| <= ||.seq2.n - seq1.n.|| by BHSP_1:38;
     then ||.seq2.n.|| - ||.seq1.n.|| < 1 by A8,AXIOMS:22;
then A9:   ||.seq2.n.|| < ||.seq1.n.|| + 1 by REAL_1:84;
       ||.seq1.n.|| <= p by A4;
     then ||.seq1.n.|| + 1 <= p + 1 by AXIOMS:24;
     hence ||.seq2.n.|| < M by A9,AXIOMS:22;
     end;
     hence thesis by A6;
     end;
       now consider M1 such that
A10:   M1 > 0 and
A11:   for n st n >= m1 holds ||.seq2.n.|| < M1 by A7;
     consider M2 such that
A12:   M2 > 0 and
A13:   for n st n <= m1 holds ||.seq2.n.|| < M2 by Th23;
     take M = M1 + M2;
       M > 0 + 0 by A10,A12,REAL_1:67;
     hence M > 0;
     A14: M > M1 + 0 by A12,REAL_1:67;
     A15: M > 0 + M2 by A10,REAL_1:67;
     let n;
A16:   now assume n >= m1;
     then ||.seq2.n.|| < M1 by A11;
     hence ||.seq2.n.|| <= M by A14,AXIOMS:22;
     end;
       now assume n <= m1;
     then ||.seq2.n.|| < M2 by A13;
     hence ||.seq2.n.|| <= M by A15,AXIOMS:22;
     end;
     hence ||.seq2.n.|| <= M by A16;
     end;
     hence thesis by Def3;
  end;

definition let X, Nseq, seq;
  redefine func seq * Nseq -> sequence of X;
coherence
         proof
         A1:   dom Nseq = NAT by FUNCT_2:def 1;
         A2:   rng seq c= the carrier of X by RELSET_1:12;
                rng Nseq c= NAT by SEQM_3:def 8;
              then rng Nseq c= dom seq by FUNCT_2:def 1;
         then A3:   dom (seq * Nseq) = NAT by A1,RELAT_1:46;
                rng (seq * Nseq) c= rng seq by RELAT_1:45;
              then rng (seq * Nseq) c= the carrier of X
              by A2,XBOOLE_1:1;
              then seq * Nseq is Function of NAT, the carrier of X
                  by A3,FUNCT_2:def 1,RELSET_1:11;
              hence thesis by NORMSP_1:def 3;
         end;
end;

definition let X be non empty 1-sorted,
               s1, s be sequence of X;
  pred s1 is_subsequence_of s means :Def4:
   ex N being increasing Seq_of_Nat st s1 = s * N;
end;

theorem Th26:
  for X being RealUnitarySpace,
      s being sequence of X,
      N being increasing Seq_of_Nat
  for n being Nat holds (s * N).n=s.(N.n)
proof
  let X be RealUnitarySpace,
      s be sequence of X,
      N be increasing Seq_of_Nat;
  let n be Nat;
    dom (s * N) = NAT by FUNCT_2:def 1;
  hence (s * N).n = s.(N.n) by FUNCT_1:22;
end;

theorem
    seq is_subsequence_of seq
proof deffunc _F(Nat) = $1;
     consider Rseq such that
A1:   for n holds Rseq.n = _F(n) from ExRealSeq;
       now let n;
         Rseq.n = n & Rseq.(n+1) = n+1 by A1;
       hence Rseq.n < Rseq.(n+1) by NAT_1:38;
     end;
then A2:   Rseq is increasing by SEQM_3:def 11;
       for n holds Rseq.n is Nat by A1;
     then reconsider Rseq as increasing Seq_of_Nat by A2,SEQM_3:29;
     take Nseq = Rseq;
       now let n;
     thus (seq * Nseq).n = seq.(Nseq.n) by Th26
                        .= seq.n by A1;
     end;
     hence thesis by FUNCT_2:113;
end;

theorem
    seq1 is_subsequence_of seq2 & seq2 is_subsequence_of seq3
    implies seq1 is_subsequence_of seq3
proof
     assume that
A1:  seq1 is_subsequence_of seq2 and
A2:  seq2 is_subsequence_of seq3;
     consider Nseq1 such that
A3:  seq1 = seq2 * Nseq1 by A1,Def4;
     consider Nseq2 such that
A4:  seq2 = seq3 * Nseq2 by A2,Def4;
     take Nseq = Nseq2 * Nseq1;
     thus seq1 = seq3 * Nseq by A3,A4,RELAT_1:55;
end;

theorem Th29:
  seq is constant & seq1 is_subsequence_of seq implies seq1 is constant
proof
     assume that
A1:  seq is constant and
A2:  seq1 is_subsequence_of seq;
     consider Nseq such that
A3:   seq1 = seq * Nseq by A2,Def4;
       now let n;
       seq.(Nseq.n) = seq.(Nseq.(n + 1)) by A1,BHSP_1:70;
     then (seq * Nseq).(n + 1) = seq.(Nseq.n) by Th26;
     hence seq1.n = seq1.(n+1) by A3,Th26;
     end;
     hence thesis by BHSP_1:68;
end;

theorem
    seq is constant & seq1 is_subsequence_of seq implies seq = seq1
proof
     assume that
A1:  seq is constant and
A2:  seq1 is_subsequence_of seq;
     consider Nseq such that
A3:   seq1 = seq * Nseq by A2,Def4;
       now let n;
     thus seq1.n = seq.(Nseq.n) by A3,Th26
                .= seq.n by A1,BHSP_1:70;
     end;
     hence thesis by FUNCT_2:113;
  end;

theorem Th31:
  seq is bounded & seq1 is_subsequence_of seq implies seq1 is bounded
proof
     assume that
A1:  seq is bounded and
A2:  seq1 is_subsequence_of seq;
     consider M1 such that
A3:  M1 > 0 and
A4:  for n holds ||.seq.n.|| <= M1 by A1,Def3;
     consider Nseq such that
A5:   seq1 = seq * Nseq by A2,Def4;
     take M = M1;
       now let n;
       seq1.n = seq.(Nseq.n) by A5,Th26;
     hence ||.seq1.n.|| <= M by A4;
     end;
     hence thesis by A3;
end;

theorem Th32:
  seq is convergent & seq1 is_subsequence_of seq implies seq1 is convergent
proof
     assume that
A1:   seq is convergent and
A2:   seq1 is_subsequence_of seq;
     consider g1 such that
A3:   for r st r > 0 ex m st for n st n >= m holds
     ||.(seq.n) - g1.|| < r by A1,BHSP_2:9;
     consider Nseq such that
A4:   seq1 = seq * Nseq by A2,Def4;
       now let r; assume r > 0;
     then consider m1 such that
A5:   for n st n >= m1 holds ||.(seq.n) - g1.|| < r by A3;
     take m = m1;
     let n such that
A6:   n >= m;
       Nseq.n >= n by SEQM_3:33;
then A7:   Nseq.n >= m by A6,AXIOMS:22;
       seq1.n = seq.(Nseq.n) by A4,Th26;
     hence ||.(seq1.n) - g1.|| < r by A5,A7;
     end;
     hence thesis by BHSP_2:9;
end;

theorem Th33:
  seq1 is_subsequence_of seq & seq is convergent implies lim seq1=lim seq
proof
     assume that
A1:   seq1 is_subsequence_of seq and
A2:   seq is convergent;
A3:   seq1 is convergent by A1,A2,Th32;
     consider Nseq such that
A4:   seq1 = seq * Nseq by A1,Def4;
       now let r; assume r > 0;
     then consider m1 such that
A5:   for n st n >= m1 holds
     dist((seq.n), (lim seq)) < r by A2,BHSP_2:def 2;
     take m = m1;
     let n such that
A6:   n >= m;
       Nseq.n >= n by SEQM_3:33;
then A7:   Nseq.n >= m by A6,AXIOMS:22;
       seq1.n = seq.(Nseq.n) by A4,Th26;
     hence dist((seq1.n), (lim seq)) < r by A5,A7;
     end;
    hence thesis by A3,BHSP_2:def 2;
end;

theorem Th34:
  seq is_Cauchy_sequence & seq1 is_subsequence_of seq
    implies seq1 is_Cauchy_sequence
proof
     assume that
A1:   seq is_Cauchy_sequence and
A2:   seq1 is_subsequence_of seq;
     consider Nseq such that
A3:   seq1 = seq * Nseq by A2,Def4;
       now let r; assume r > 0;
     then consider l such that
A4:   for n, m st ( n >= l & m >= l )
     holds dist((seq.n), (seq.m)) < r by A1,Def1;
     take k = l;
     let n, m such that
A5:   n >= k & m >= k;
       Nseq.n >= n & Nseq.m >= m by SEQM_3:33;
then A6:   Nseq.n >= k & Nseq.m >= k by A5,AXIOMS:22;
       seq1.n = seq.(Nseq.n) &
     seq1.m = seq.(Nseq.m) by A3,Th26;
     hence dist((seq1.n), (seq1.m)) < r by A4,A6;
     end;
     hence thesis by Def1;
end;

definition
          let X;
          let seq;
          let k;
          func seq ^\k -> sequence of X means
:Def5:  for n holds it.n=seq.(n + k);
existence proof deffunc _F(Nat) = seq.($1 + k);
  thus ex IT being sequence of X st for n holds IT.n=_F(n) from Ex_Seq_in_RUS;
end;
uniqueness
          proof
              let seq1, seq2;
              assume that
          A1: for n holds seq1.n = seq.(n + k) and
          A2: for n holds seq2.n = seq.(n + k);
                now let n;
              seq1.n = seq.(n + k) by A1;
              hence seq1.n = seq2.n by A2;
              end;
              hence seq1 = seq2 by FUNCT_2:113;
          end;
end;

theorem
    seq ^\0 = seq
proof
       now let n;
     thus (seq ^\0).n = seq.(n + 0) by Def5
                    .= seq.n;
     end;
     hence thesis by FUNCT_2:113;
 end;

theorem
    (seq ^\k)^\m = (seq ^\m)^\k
proof
       now let n;
     thus ((seq ^\k)^\m).n = (seq ^\k).(n + m) by Def5
                        .= seq.(n + m + k) by Def5
                        .= seq.(n + k + m) by XCMPLX_1:1
                        .= (seq ^\m).(n + k) by Def5
                        .= ((seq ^\m)^\k).n by Def5;
     end;
     hence thesis by FUNCT_2:113;
end;

theorem
    (seq ^\k)^\m=seq ^\(k + m)
proof
       now let n;
     thus
       ((seq ^\k)^\m).n = (seq ^\k).(n + m) by Def5
                   .= seq.(n + m + k) by Def5
                   .= seq.(n + (k + m)) by XCMPLX_1:1
                   .= (seq ^\(k + m)).n by Def5;
     end;
     hence thesis by FUNCT_2:113;
  end;

theorem Th38:
  (seq1 + seq2) ^\k = (seq1 ^\k) + (seq2 ^\k)
proof
       now let n;
     thus
       ((seq1 + seq2) ^\k).n = (seq1 + seq2).(n + k) by Def5
                         .= seq1.(n + k) + seq2.(n + k) by NORMSP_1:def 5
                         .= (seq1 ^\k).n + seq2.(n + k) by Def5
                         .= (seq1 ^\k).n + (seq2 ^\k).n by Def5
                         .= ((seq1 ^\k) + (seq2 ^\k)).n by NORMSP_1:def 5;
     end;
     hence thesis by FUNCT_2:113;
end;

theorem Th39:
  (-seq) ^\k = -(seq ^\k)
proof
       now let n;
     thus
       ((-seq) ^\k).n = (-seq).(n + k) by Def5
                  .= -(seq.(n + k)) by BHSP_1:def 10
                  .= -((seq ^\ k).n) by Def5
                  .= (-(seq ^\k)).n by BHSP_1:def 10;
     end;
     hence thesis by FUNCT_2:113;
end;

theorem
    (seq1 - seq2) ^\k = (seq1 ^\k) - (seq2 ^\k)
proof
     thus
       (seq1 - seq2) ^\k = (seq1 + (-seq2)) ^\k by BHSP_1:71
                     .= (seq1 ^\k) + ((-seq2) ^\k) by Th38
                     .= (seq1 ^\k) + -(seq2 ^\k) by Th39
                     .= (seq1 ^\k) - (seq2 ^\k) by BHSP_1:71;
end;

theorem
    (a * seq) ^\k = a * (seq ^\k)
proof
       now let n;
     thus
       ((a * seq) ^\k).n = (a * seq).(n + k) by Def5
                     .= a * (seq.(n + k)) by NORMSP_1:def 8
                     .= a * ((seq ^\k).n) by Def5
                     .= (a * (seq ^\k)).n by NORMSP_1:def 8;
     end;
     hence thesis by FUNCT_2:113;
end;

theorem
    (seq * Nseq) ^\k = seq * (Nseq ^\k)
proof
       now let n;
     thus
       ((seq * Nseq) ^\k).n = (seq * Nseq).(n + k) by Def5
                        .= seq.(Nseq.(n + k)) by Th26
                        .= seq.((Nseq ^\k).n) by SEQM_3:def 9
                        .= (seq * (Nseq ^\k)).n by Th26;
     end;
     hence thesis by FUNCT_2:113;
end;

theorem Th43:
  seq ^\k is_subsequence_of seq
proof deffunc _F(Nat) = $1 + k;
     consider Rseq such that
A1:   for n holds Rseq.n = _F(n) from ExRealSeq;
       now let n;
A2:   Rseq.n = n + k & Rseq.(n + 1) = n + 1 + k by A1;
       n + k < n + k + 1 by NAT_1:38;
     hence Rseq.n < Rseq.(n + 1) by A2,XCMPLX_1:1;
     end;
then A3:   Rseq is increasing by SEQM_3:def 11;
       now let n;
       n + k is Nat;
     hence Rseq.n is Nat by A1;
     end;
     then reconsider Rseq as increasing Seq_of_Nat by A3,SEQM_3:29;
     take Nseq=Rseq;
       now let n;
     thus
       (seq * Nseq).n = seq.(Nseq.n) by Th26
                   .= seq.(n + k) by A1
                   .= (seq ^\k).n by Def5;
     end;
     hence thesis by FUNCT_2:113;
  end;

theorem
    seq is convergent implies ((seq ^\k) is convergent &
     lim (seq ^\k)=lim seq)
proof
    assume
A1:  seq is convergent;
A2:  seq ^\k is_subsequence_of seq by Th43;
    hence seq ^\k is convergent by A1,Th32;
    thus lim (seq ^\k) = lim seq by A1,A2,Th33;
end;

canceled;

theorem
    seq is convergent & (ex k st seq = seq1 ^\k) implies seq1 is convergent
proof
     assume that
A1:   seq is convergent and
A2:   ex k st seq = seq1 ^\k;
     consider k such that
A3:   seq = seq1 ^\k by A2;
     consider g1 such that
A4:   for r st r > 0 ex m st for n st n >= m holds
     ||.seq.n - g1.|| < r by A1,BHSP_2:9;
       now take g = g1;
     let r; assume r > 0;
     then consider m1 such that
A5:   for n st n >= m1 holds ||.seq.n - g.|| < r by A4;
     take m = m1 + k;
     let n; assume
A6:   n >= m;
     then consider m2 such that
A7:   n = m1 + k + m2 by NAT_1:28;
       n - k = m1 + k + m2 + -k by A7,XCMPLX_0:def 8
          .= m1 + m2 + k + -k by XCMPLX_1:1
          .= m1 + m2 + k - k by XCMPLX_0:def 8
          .= m1 + m2 + (k - k) by XCMPLX_1:29
          .= m1 + m2 + 0 by XCMPLX_1:14
          .= m1 + m2;
     then consider l such that
A8:   l = n - k;
A9:   now assume l < m1;
     then l + k < m1 + k by REAL_1:53;
     then n - (k - k) < m1 + k by A8,XCMPLX_1:37;
     then n - 0 < m1 + k by XCMPLX_1:14;
     hence contradiction by A6;
     end;
A10:   l + k = n - (k - k) by A8,XCMPLX_1:37
           .= n - 0 by XCMPLX_1:14
           .= n;
       ||.seq.l - g.|| < r by A5,A9;
     hence ||.seq1.n - g.|| < r by A3,A10,Def5;
     end;
     hence thesis by BHSP_2:9;
 end;

theorem
    seq is_Cauchy_sequence & (ex k st seq = seq1 ^\k)
    implies seq1 is_Cauchy_sequence
proof
     assume that
A1:   seq is_Cauchy_sequence and
A2:   ex k st seq = seq1 ^\k;
     consider k such that
A3:   seq = seq1 ^\k by A2;
     let r; assume r > 0;
     then consider l1 such that
A4:   for n, m st ( n >= l1 & m >= l1 ) holds
     dist((seq.n), (seq.m)) < r by A1,Def1;
     take l = l1 + k;
     let n, m; assume
A5:   n >= l & m >= l;
     then consider m1 such that
A6:   n = l1 + k + m1 by NAT_1:28;
A7:   n - k = l1 + k + m1 + -k by A6,XCMPLX_0:def 8
          .= l1 + m1 + k + -k by XCMPLX_1:1
          .= l1 + m1 + k - k by XCMPLX_0:def 8
          .= l1 + m1 + (k - k) by XCMPLX_1:29
          .= l1 + m1 + 0 by XCMPLX_1:14
          .= l1 + m1;
     consider m2 such that
A8:   m = l1 + k + m2 by A5,NAT_1:28;
A9:   m - k = l1 + k + m2 + -k by A8,XCMPLX_0:def 8
          .= l1 + m2 + k + -k by XCMPLX_1:1
          .= l1 + m2 + k - k by XCMPLX_0:def 8
          .= l1 + m2 + (k - k) by XCMPLX_1:29
          .= l1 + m2 + 0 by XCMPLX_1:14
          .= l1 + m2;
     consider l2 such that
A10:   l2 = n - k by A7;
A11:   now assume l2 < l1;
     then l2 + k < l1 + k by REAL_1:53;
     then n - (k - k) < l1 + k by A10,XCMPLX_1:37;
     then n - 0 < l1 + k by XCMPLX_1:14;
     hence contradiction by A5;
     end;
     consider l3 such that
A12:   l3 = m - k by A9;
A13:   now assume l3 < l1;
     then l3 + k < l1 + k by REAL_1:53;
     then m - (k - k) < l1 + k by A12,XCMPLX_1:37;
     then m - 0 < l1 + k by XCMPLX_1:14;
     hence contradiction by A5;
     end;
A14:   l2 + k = n - (k - k) by A10,XCMPLX_1:37
           .= n - 0 by XCMPLX_1:14
           .= n;
A15:   l3 + k = m - (k - k) by A12,XCMPLX_1:37
           .= m - 0 by XCMPLX_1:14
           .= m;
        dist((seq.l2), (seq.l3)) < r by A4,A11,A13;
      then dist((seq1.n), (seq.l3)) < r by A3,A14,Def5;
      hence dist((seq1.n), (seq1.m)) < r by A3,A15,Def5;
end;

theorem
    seq is_Cauchy_sequence implies (seq ^\k) is_Cauchy_sequence
proof
    assume
A1:  seq is_Cauchy_sequence;
      seq ^\k is_subsequence_of seq by Th43;
    hence thesis by A1,Th34;
end;

theorem
    seq1 is_compared_to seq2 implies (seq1 ^\k) is_compared_to (seq2 ^\k)
proof
     assume
A1:     seq1 is_compared_to seq2;
     let r; assume r > 0;
     then consider m1 such that
A2:   for n st n >= m1 holds
     dist((seq1.n), (seq2.n)) < r by A1,Def2;
     take m = m1;
     let n such that
A3:   n >= m;
       n + k >= n by NAT_1:29;
     then n + k >= m by A3,AXIOMS:22;
     then dist((seq1.(n + k)), (seq2.(n + k))) < r by A2;
     then dist((seq1 ^\k).n, (seq2.(n + k))) < r by Def5;
     hence dist((seq1 ^\k).n, (seq2 ^\k).n) < r by Def5;
end;

theorem
    seq is bounded implies (seq ^\k) is bounded
proof
    assume
A1:  seq is bounded;
      seq ^\k is_subsequence_of seq by Th43;
    hence thesis by A1,Th31;
end;

theorem
    seq is constant implies (seq ^\k) is constant
proof
    assume
A1:  seq is constant;
      seq ^\k is_subsequence_of seq by Th43;
    hence thesis by A1,Th29;
end;

definition
          let X;
          attr X is complete means
:Def6:    for seq holds
          seq is_Cauchy_sequence implies seq is convergent;
  synonym X is_complete_space;
end;

canceled;

theorem
    X is_complete_space & seq is_Cauchy_sequence implies seq is bounded
proof
     assume that
A1:   X is_complete_space and
A2:   seq is_Cauchy_sequence;
       seq is convergent by A1,A2,Def6;
     hence thesis by Th24;
end;

definition
          let X;
          attr X is Hilbert means
            X is RealUnitarySpace & X is_complete_space;
  synonym X is_Hilbert_space;
end;

Back to top