:: Introduction to Banach and Hilbert spaces - Part II
::  by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2019 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, BHSP_1, PRE_TOPC, REAL_1, NAT_1, SUBSET_1, SUPINF_2,
      SEQ_2, XXREAL_0, CARD_1, METRIC_1, FUNCT_1, ARYTM_3, ARYTM_1, RELAT_1,
      COMPLEX1, NORMSP_1, ORDINAL2, SEQ_1, TARSKI, STRUCT_0, XBOOLE_0;
 notations TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
      REAL_1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, RELAT_1, VALUED_0, STRUCT_0,
      PRE_TOPC, RLVECT_1, VFUNCT_1, BHSP_1, NORMSP_1, XXREAL_0;
 constructors DOMAIN_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQ_2, BHSP_1,
      VALUED_1, RELSET_1, VFUNCT_1, COMSEQ_2;
 registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, VFUNCT_1, FUNCT_2, NAT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems TARSKI, NAT_1, FUNCT_1, SEQ_2, ABSVALUE, SUBSET_1, RLVECT_1, BHSP_1,
      NORMSP_1, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_1, COMPLEX1,
      XXREAL_0, VALUED_0, ORDINAL1;
 schemes SEQ_1, FRAENKEL;

begin

reserve X for RealUnitarySpace;
reserve x, y, z, g, g1, g2 for Point of X;
reserve a, q, r for Real;
reserve seq, seq1, seq2, seq9 for sequence of X;
reserve k, n, m, m1, m2 for Nat;

deffunc 09(RealUnitarySpace) = 0. $1;

definition
  let X, seq;
  attr seq is convergent means

  ex g st for r st r > 0 ex m st for n st n >= m holds dist(seq.n, g) < r;
end;

registration let X;
 cluster constant -> convergent for sequence of X;
 coherence
proof let seq be sequence of X;
 assume seq is constant;
 then consider x such that
A1: for n being Nat holds seq.n = x by VALUED_0:def 18;
  take g = x;
  let r such that
A2: r > 0;
  take m = 0;
  let n such that
  n >= m;
  dist(seq.n, g) = dist(x, g) by A1
    .= 0 by BHSP_1:34;
  hence thesis by A2;
end;
end;

theorem
  seq is constant implies seq is convergent;

theorem Th2:
  seq is convergent & (ex k st for n st k <= n holds seq9.n = seq.n
  ) implies seq9 is convergent
proof
  assume that
A1: seq is convergent and
A2: ex k st for n st k <= n holds seq9.n = seq.n;
  consider k such that
A3: for n st n >= k holds seq9.n = seq.n by A2;
  consider g such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r
  by A1;
  take h = g;
  let r;
  assume r > 0;
  then consider m1 such that
A5: for n st n >= m1 holds dist((seq.n) , h) < r by A4;
A6: now
    assume
A7: m1 <= k;
    take m = k;
    let n;
    assume
A8: n >= m;
    then n >= m1 by A7,XXREAL_0:2;
    then dist((seq.n) , g) < r by A5;
    hence dist((seq9.n) , h) < r by A3,A8;
  end;
  now
    assume
A9: k <= m1;
    take m = m1;
    let n;
    assume
A10: n >= m;
    then seq9.n = seq.n by A3,A9,XXREAL_0:2;
    hence dist((seq9.n) , h) < r by A5,A10;
  end;
  hence thesis by A6;
end;

theorem Th3:
  seq1 is convergent & seq2 is convergent implies seq1 + seq2 is convergent
proof
  assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
  consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq1.n) , g1) < r
  by A1;
  consider g2 such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq2.n) , g2) < r
  by A2;
  take g = g1 + g2;
  let r;
  assume
A5: r > 0;
  then consider m1 such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3,XREAL_1:215;
  consider m2 such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5,XREAL_1:215;
   reconsider k = m1 + m2 as Nat;
  take k;
  let n be Nat such that
A8: n >= k;
  k >= m2 by NAT_1:12;
  then n >= m2 by A8,XXREAL_0:2;
  then
A9: dist((seq2.n) , g2) < r/2 by A7;
  dist((seq1 + seq2).n, g) = dist((seq1.n) + (seq2.n) , (g1 + g2)) by
NORMSP_1:def 2;
  then
A10: dist((seq1 + seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
  by BHSP_1:40;
  m1 + m2 >= m1 by NAT_1:12;
  then n >= m1 by A8,XXREAL_0:2;
  then dist((seq1.n) , g1) < r/2 by A6;
  then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A9,XREAL_1:8;
  hence thesis by A10,XXREAL_0:2;
end;

theorem Th4:
  seq1 is convergent & seq2 is convergent implies seq1 - seq2 is convergent
proof
  assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
  consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq1.n) , g1) < r
  by A1;
  consider g2 such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq2.n) , g2) < r
  by A2;
  take g = g1 - g2;
  let r;
  assume
A5: r > 0;
  then consider m1 such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3,XREAL_1:215;
  consider m2 such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5,XREAL_1:215;
  take k = m1 + m2;
  let n such that
A8: n >= k;
  k >= m2 by NAT_1:12;
  then n >= m2 by A8,XXREAL_0:2;
  then
A9: dist((seq2.n) , g2) < r/2 by A7;
  dist((seq1 - seq2).n, g) = dist((seq1.n) - (seq2.n) , (g1 - g2)) by
NORMSP_1:def 3;
  then
A10: dist((seq1 - seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
  by BHSP_1:41;
  m1 + m2 >= m1 by NAT_1:12;
  then n >= m1 by A8,XXREAL_0:2;
  then dist((seq1.n) , g1) < r/2 by A6;
  then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A9,XREAL_1:8;
  hence thesis by A10,XXREAL_0:2;
end;

theorem Th5:
  seq is convergent implies a * seq is convergent
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 dist((seq.n) , g) < r;
  take h = a * g;
A2: now
A3: 0/|.a.| = 0;
    assume
A4: a <> 0;
    then
A5: |.a.| > 0 by COMPLEX1:47;
    let r;
    assume r > 0;
    then consider m1 such that
A6: for n st n >= m1 holds dist(seq.n, g) < r/|.a.| by A1,A5,A3,XREAL_1:74;
    take k = m1;
    let n;
    assume n >= k;
    then
A7: dist((seq.n) , g) < r/|.a.| by A6;
A8: |.a.| <> 0 by A4,COMPLEX1:47;
A9: |.a.| * (r/|.a.|) = |.a.| * (|.a.|" * r) by XCMPLX_0:def 9
      .= |.a.| *|.a.|" * r
      .= 1 * r by A8,XCMPLX_0:def 7
      .= r;
    dist(a * (seq.n) , a * g) = ||.(a * (seq.n)) - (a * g).|| by BHSP_1:def 5
      .= ||.a * ((seq.n) - g).|| by RLVECT_1:34
      .= |.a.| * ||.(seq.n) - g.|| by BHSP_1:27
      .= |.a.| * dist((seq.n) , g) by BHSP_1:def 5;
    then dist((a *(seq.n)) , h) < r by A5,A7,A9,XREAL_1:68;
    hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
  end;
  now
    assume
A10: a = 0;
    let r;
    assume r > 0;
    then consider m1 such that
A11: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
    take k = m1;
    let n;
    assume n >= k;
    then
A12: dist((seq.n) , g) < r by A11;
    dist(a * (seq.n) , a * g) = dist(0 * (seq.n) , 09(X)) by A10,RLVECT_1:10
      .= dist(09(X) , 09(X)) by RLVECT_1:10
      .= 0 by BHSP_1:34;
    then dist(a * (seq.n) , h) < r by A12,BHSP_1:37;
    hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
  end;
  hence thesis by A2;
end;

theorem Th6:
  seq is convergent implies - seq is convergent
proof
  assume seq is convergent;
  then (-1) * seq is convergent by Th5;
  hence thesis by BHSP_1:55;
end;

theorem Th7:
  seq is convergent implies seq + x is convergent
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 dist((seq.n) , g) < r;
  take g + x;
  let r;
  assume r > 0;
  then consider m1 such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
  take k = m1;
  let n;
  dist((seq.n) + x, g + x) <= dist((seq.n) , g) + dist(x, x) by BHSP_1:40;
  then
A3: dist((seq.n) + x, g + x) <= dist((seq.n) , g) + 0 by BHSP_1:34;
  assume n >= k;
  then dist((seq.n) , g) < r by A2;
  then dist((seq.n) + x, g + x) < r by A3,XXREAL_0:2;
  hence thesis by BHSP_1:def 6;
end;

theorem Th8:
  seq is convergent implies seq - x is convergent
proof
  assume seq is convergent;
  then seq + (-x) is convergent by Th7;
  hence thesis by BHSP_1:56;
end;

theorem Th9:
  seq is convergent iff ex g st for r st r > 0 ex m st for n st n
  >= m holds ||.(seq.n) - g.|| < r
proof
  thus seq is convergent implies ex g st for r st r > 0 ex m st for n st n >=
  m holds ||.(seq.n) - g.|| < r
  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 dist((seq.n) , g) < r;
    take g;
    let r;
    assume r > 0;
    then consider m1 such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
    take k = m1;
    let n;
    assume n >= k;
    then dist((seq.n) , g) < r by A2;
    hence thesis by BHSP_1:def 5;
  end;
  ( ex g st for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.||
  < r ) implies seq is convergent
  proof
    given g such that
A3: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r;
    take g;
    let r;
    assume r > 0;
    then consider m1 such that
A4: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A3;
    take k = m1;
    let n;
    assume n >= k;
    then ||.(seq.n) - g.|| < r by A4;
    hence thesis by BHSP_1:def 5;
  end;
  hence thesis;
end;

definition
  let X, seq;
  assume
A1: seq is convergent;
  func lim seq -> Point of X means
  :Def2:
  for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , it) < r;
  existence by A1;
  uniqueness
  proof
    for x, y st ( for r st r > 0 ex m st for n st n >= m holds dist((seq.n
) , x) < r ) & ( for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y)
    < r ) holds x = y
    proof
      given x, y such that
A2:   for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , x) < r and
A3:   for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y) < r and
A4:   x <> y;
A5:   dist(x, y) > 0 by A4,BHSP_1:38;
      then
A6:   dist(x, y)/4 > 0/4 by XREAL_1:74;
      then consider m1 such that
A7:   for n st n >= m1 holds dist((seq.n) , x) < dist(x, y)/4 by A2;
      consider m2 such that
A8:   for n st n >= m2 holds dist((seq.n) , y) < dist(x, y)/4 by A3,A6;
A9:   now
        assume m1 >= m2;
        then
A10:    dist((seq.m1) , y) < dist(x, y)/4 by A8;
        dist(x, y) = dist(x - (seq.m1) , y - (seq.m1)) by BHSP_1:42;
        then
A11:    dist(x, y) <= dist((seq.m1) , x) + dist((seq.m1) , y) by BHSP_1:43;
        dist((seq.m1) , x) < dist(x, y)/4 by A7;
        then dist((seq.m1) , x) + dist((seq.m1) , y) < dist(x, y)/4 + dist(x,
        y) /4 by A10,XREAL_1:8;
        then dist(x, y) <= dist(x, y)/2 by A11,XXREAL_0:2;
        hence contradiction by A5,XREAL_1:216;
      end;
      now
        assume m1 <= m2;
        then
A12:    dist((seq.m2) , x) < dist(x, y)/4 by A7;
        dist(x, y) = dist(x - (seq.m2) , y - (seq.m2)) by BHSP_1:42;
        then
A13:    dist(x, y) <= dist((seq.m2) , x) + dist((seq.m2) , y) by BHSP_1:43;
        dist((seq.m2) , y) < dist(x, y)/4 by A8;
        then dist((seq.m2) , x) + dist((seq.m2) , y) < dist(x, y)/4 + dist(x,
        y)/4 by A12,XREAL_1:8;
        then dist(x, y) <= dist(x, y)/2 by A13,XXREAL_0:2;
        hence contradiction by A5,XREAL_1:216;
      end;
      hence contradiction by A9;
    end;
    hence thesis;
  end;
end;

theorem Th10:
  seq is constant & x in rng seq implies lim seq = x
proof
  assume that
A1: seq is constant and
A2: x in rng seq;
  consider y such that
A3: rng seq = {y} by A1,FUNCT_2:111;
  consider z such that
A4: for n being Nat holds seq.n = z by A1,VALUED_0:def 18;
A5: x = y by A2,A3,TARSKI:def 1;
A6: now
    let r such that
A7: r > 0;
     reconsider m = 0 as Nat;
    take m;
    let n such that
    n >= m;
  n in NAT by ORDINAL1:def 12;
    then n in dom seq by NORMSP_1:12;
    then seq.n in rng seq by FUNCT_1:def 3;
    then z in rng seq by A4;
    then z = x by A3,A5,TARSKI:def 1;
    then seq.n = x by A4;
    hence dist((seq.n) , x) < r by A7,BHSP_1:34;
  end;
  seq is convergent by A1;
  hence thesis by A6,Def2;
end;

theorem
  seq is constant & (ex n st seq.n = x) implies lim seq = x
proof
  assume that
A1: seq is constant and
A2: ex n st seq.n = x;
  consider n such that
A3: seq.n = x by A2;
  n in NAT by ORDINAL1:def 12;
  then n in dom seq by NORMSP_1:12;
  then x in rng seq by A3,FUNCT_1:def 3;
  hence thesis by A1,Th10;
end;

theorem
  seq is convergent & (ex k st for n st n >= k holds seq9.n = seq.n)
  implies lim seq = lim seq9
proof
  assume that
A1: seq is convergent and
A2: ex k st for n st n >= k holds seq9.n = seq.n;
  consider k such that
A3: for n st n >= k holds seq9.n = seq.n by A2;
A4: 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 A1,Def2;
A6: now
      assume
A7:   m1 <= k;
      take m = k;
      let n;
      assume
A8:   n >= m;
      then n >= m1 by A7,XXREAL_0:2;
      then dist((seq.n) , (lim seq)) < r by A5;
      hence dist((seq9.n) , (lim seq)) < r by A3,A8;
    end;
    now
      assume
A9:   k <= m1;
      take m = m1;
      let n;
      assume
A10:  n >= m;
      then seq9.n = seq.n by A3,A9,XXREAL_0:2;
      hence dist((seq9.n) , (lim seq)) < r by A5,A10;
    end;
    hence ex m st for n st n >= m holds dist((seq9.n) , (lim seq)) < r by A6;
  end;
  seq9 is convergent by A1,A2,Th2;
  hence thesis by A4,Def2;
end;

theorem Th13:
  seq1 is convergent & seq2 is convergent implies lim (seq1 + seq2
  ) = (lim seq1) + (lim seq2)
proof
  assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
  set g2 = lim seq2;
  set g1 = lim seq1;
  set g = g1 + g2;
A3: now
    let r;
    assume r > 0;
    then
A4: r/2 > 0 by XREAL_1:215;
    then consider m1 such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
    consider m2 such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
    take k = m1 + m2;
    let n such that
A7: n >= k;
    k >= m2 by NAT_1:12;
    then n >= m2 by A7,XXREAL_0:2;
    then
A8: dist((seq2.n) , g2) < r/2 by A6;
    dist((seq1 + seq2).n, g) = dist((seq1.n) + (seq2.n) , g1 + g2) by
NORMSP_1:def 2;
    then
A9: dist((seq1 + seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
    by BHSP_1:40;
    m1 + m2 >= m1 by NAT_1:12;
    then n >= m1 by A7,XXREAL_0:2;
    then dist((seq1.n) , g1) < r/2 by A5;
    then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A8,XREAL_1:8;
    hence dist((seq1 + seq2).n, g) < r by A9,XXREAL_0:2;
  end;
  seq1 + seq2 is convergent by A1,A2,Th3;
  hence thesis by A3,Def2;
end;

theorem Th14:
  seq1 is convergent & seq2 is convergent implies lim (seq1 - seq2
  ) = (lim seq1) - (lim seq2)
proof
  assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
  set g2 = lim seq2;
  set g1 = lim seq1;
  set g = g1 - g2;
A3: now
    let r;
    assume r > 0;
    then
A4: r/2 > 0 by XREAL_1:215;
    then consider m1 such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
    consider m2 such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
    take k = m1 + m2;
    let n such that
A7: n >= k;
    k >= m2 by NAT_1:12;
    then n >= m2 by A7,XXREAL_0:2;
    then
A8: dist((seq2.n) , g2) < r/2 by A6;
    dist((seq1 - seq2).n, g) = dist((seq1.n) - (seq2.n) , g1 - g2) by
NORMSP_1:def 3;
    then
A9: dist((seq1 - seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
    by BHSP_1:41;
    m1 + m2 >= m1 by NAT_1:12;
    then n >= m1 by A7,XXREAL_0:2;
    then dist((seq1.n) , g1) < r/2 by A5;
    then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A8,XREAL_1:8;
    hence dist((seq1 - seq2).n, g) < r by A9,XXREAL_0:2;
  end;
  seq1 - seq2 is convergent by A1,A2,Th4;
  hence thesis by A3,Def2;
end;

theorem Th15:
  seq is convergent implies lim (a * seq) = a * (lim seq)
proof
  set g = lim seq;
  set h = a * g;
  assume
A1: seq is convergent;
A2: now
    assume
A3: a = 0;
    let r;
    assume r > 0;
    then consider m1 such that
A4: for n st n >= m1 holds dist((seq.n) , g) < r by A1,Def2;
    take k = m1;
    let n;
    assume n >= k;
    then
A5: dist((seq.n) , g) < r by A4;
    dist(a * (seq.n) , a * g) = dist(0 * (seq.n) , 09(X)) by A3,RLVECT_1:10
      .= dist(09(X) , 09(X)) by RLVECT_1:10
      .= 0 by BHSP_1:34;
    then dist(a * (seq.n) , h) < r by A5,BHSP_1:37;
    hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
  end;
A6: now
A7: 0/|.a.| =0;
    assume
A8: a <> 0;
    then
A9: |.a.| > 0 by COMPLEX1:47;
    let r;
    assume r > 0;
    then r/|.a.| > 0 by A9,A7,XREAL_1:74;
    then consider m1 such that
A10: for n st n >= m1 holds dist((seq.n) , g) < r/|.a.| by A1,Def2;
    take k = m1;
    let n;
    assume n >= k;
    then
A11: dist((seq.n) , g) < r/|.a.| by A10;
A12: |.a.| <> 0 by A8,COMPLEX1:47;
A13: |.a.| * (r/|.a.|) = |.a.| * (|.a.|" * r) by XCMPLX_0:def 9
      .= |.a.| *|.a.|" * r
      .= 1 * r by A12,XCMPLX_0:def 7
      .= r;
    dist(a * (seq.n) , a * g) = ||.(a * (seq.n)) - (a * g).|| by BHSP_1:def 5
      .= ||.a * ((seq.n) - g).|| by RLVECT_1:34
      .= |.a.| * ||.(seq.n) - g.|| by BHSP_1:27
      .= |.a.| * dist((seq.n) , g) by BHSP_1:def 5;
    then dist(a * (seq.n) , h) < r by A9,A11,A13,XREAL_1:68;
    hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
  end;
  a * seq is convergent by A1,Th5;
  hence thesis by A2,A6,Def2;
end;

theorem Th16:
  seq is convergent implies lim (- seq) = - (lim seq)
proof
  assume seq is convergent;
  then lim ((-1) * seq) = (-1) * (lim seq) by Th15;
  then lim (- seq) = (-1) * (lim seq) by BHSP_1:55;
  hence thesis by RLVECT_1:16;
end;

theorem Th17:
  seq is convergent implies lim (seq + x) = (lim seq) + x
proof
  set g = lim seq;
  assume
A1: seq is convergent;
A2: now
    let r;
    assume r > 0;
    then consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,Def2;
    take k = m1;
    let n;
    assume n >= k;
    then
A4: dist((seq.n) , g) < r by A3;
    dist((seq.n) , g) = dist((seq.n) - (-x) , g - (-x)) by BHSP_1:42
      .= dist((seq.n) + (-(-x)) , g - (-x)) by RLVECT_1:def 11
      .= dist((seq.n) + x, g - (-x)) by RLVECT_1:17
      .= dist((seq.n) + x, g + (-(-x))) by RLVECT_1:def 11
      .= dist((seq.n) + x, g + x) by RLVECT_1:17;
    hence dist((seq + x).n, (g + x)) < r by A4,BHSP_1:def 6;
  end;
  seq + x is convergent by A1,Th7;
  hence thesis by A2,Def2;
end;

theorem
  seq is convergent implies lim (seq - x) = (lim seq) - x
proof
  assume seq is convergent;
  then lim (seq + (-x)) = (lim seq) + (-x) by Th17;
  then lim (seq - x) = (lim seq) + (-x) by BHSP_1:56;
  hence thesis by RLVECT_1:def 11;
end;

theorem Th19:
  seq is convergent implies ( lim seq = g iff for r st r > 0 ex m
  st for n st n >= m holds ||.(seq.n) - g.|| < r )
proof
  assume
A1: seq is convergent;
  thus lim seq = g implies for r st r > 0 ex m st for n st n >= m holds ||.(
  seq.n) - g.|| < r
  proof
    assume
A2: lim seq = g;
    let r;
    assume r > 0;
    then consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,Def2;
    take k = m1;
    let n;
    assume n >= k;
    then dist((seq.n) , g) < r by A3;
    hence thesis by BHSP_1:def 5;
  end;
  ( for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r )
  implies lim seq = g
  proof
    assume
A4: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r;
    now
      let r;
      assume r > 0;
      then consider m1 such that
A5:   for n st n >= m1 holds ||.(seq.n) - g.|| < r by A4;
      take k = m1;
      let n;
      assume n >= k;
      then ||.(seq.n) - g.|| < r by A5;
      hence dist((seq.n) , g) < r by BHSP_1:def 5;
    end;
    hence thesis by A1,Def2;
  end;
  hence thesis;
end;

definition
  let X, seq;
  func ||.seq.|| -> Real_Sequence means
  :Def3:
  for n holds it.n =||.(seq.n).||;
  existence
  proof
    deffunc F(Nat) = ||.(seq.$1).||;
    consider s being Real_Sequence such that
A1: for n being Nat holds s.n = F(n) from SEQ_1:sch 1;
    take s;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let s,t be Real_Sequence;
    assume that
A2: for n holds s.n = ||.(seq.n).|| and
A3: for n holds t.n = ||.(seq.n).||;
    now
      let n be Element of NAT;
      s.n = ||.(seq.n).|| by A2;
      hence s.n = t.n by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th20:
  seq is convergent implies ||.seq.|| is convergent
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 Th9;
  now
    let r be Real;
    assume
A2: r > 0;
    consider m1 such that
A3: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2;
     reconsider k = m1 as Nat;
    take k;
    now
      let n be Nat;
      assume n >= k;
      then
A4:   ||.(seq.n) - g.|| < r by A3;
      |.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by BHSP_1:33;
      then |.||.(seq.n).|| - ||.g.||.| < r by A4,XXREAL_0:2;
      hence |.||.seq.||.n - ||.g.||.| < r by Def3;
    end;
    hence for n being Nat st k <= n holds |.||.seq.||.n - ||.g.||.| < r;
  end;
  hence thesis by SEQ_2:def 6;
end;

theorem Th21:
  seq is convergent & lim seq = g implies ||.seq.|| is convergent
  & lim ||.seq.|| = ||.g.||
proof
  assume that
A1: seq is convergent and
A2: lim seq = g;
A3: now
    let r be Real;
    assume
A4: r > 0;
    consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,Th19;
     reconsider k = m1 as Nat;
    take k;
    now
      let n be Nat;
      assume n >= k;
      then
A6:   ||.(seq.n) - g.|| < r by A5;
      |.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by BHSP_1:33;
      then |.||.(seq.n).|| - ||.g.||.| < r by A6,XXREAL_0:2;
      hence |.||.seq.||.n - ||.g.||.| < r by Def3;
    end;
    hence for n being Nat st k <= n holds |.||.seq.||.n - ||.g.||.| < r;
  end;
  ||.seq.|| is convergent by A1,Th20;
  hence thesis by A3,SEQ_2:def 7;
end;

theorem Th22:
  seq is convergent & lim seq = g implies ||.seq - g.|| is
  convergent & lim ||.seq - g.|| = 0
proof
  assume that
A1: seq is convergent and
A2: lim seq = g;
A3: now
    let r be Real;
    assume
A4: r > 0;
    consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,Th19;
     reconsider k = m1 as Nat;
    take k;
    let n be Nat;
    assume n >= k;
    then ||.(seq.n) - g.|| < r by A5;
    then
A6: ||.((seq.n) - g ) - 09(X).|| < r by RLVECT_1:13;
    |.||.(seq.n) - g.|| - ||.09(X).||.| <= ||.((seq.n) - g ) - 09( X )
    .|| by BHSP_1:33;
    then |.||.(seq.n) - g.|| - ||.09(X).||.| < r by A6,XXREAL_0:2;
    then |.(||.(seq.n) - g.|| - 0).| < r by BHSP_1:26;
    then |.(||.(seq - g).n.|| - 0).| < r by NORMSP_1:def 4;
    hence |.(||.seq - g.||.n - 0).| < r by Def3;
  end;
  ||.seq - g.|| is convergent by A1,Th8,Th20;
  hence thesis by A3,SEQ_2:def 7;
end;

definition
  let X;
  let seq;
  let x;
  func dist(seq, x) -> Real_Sequence means
  :Def4:
  for n holds it.n =dist((seq. n) , x);
  existence
  proof
    deffunc F(Nat) = dist((seq.$1) , x);
    consider s being Real_Sequence such that
A1: for n being Nat holds s.n = F(n) from SEQ_1:sch 1;
    take s;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let s,t be Real_Sequence;
    assume that
A2: for n holds s.n = dist((seq.n) , x) and
A3: for n holds t.n = dist((seq.n) , x);
    now
      let n be Element of NAT;
      s.n = dist((seq.n) , x) by A2;
      hence s.n = t.n by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th23:
  seq is convergent & lim seq = g implies dist(seq, g) is convergent
proof
  assume
A1: seq is convergent & lim seq = g;
  now
    let r be Real;
    assume
A2: r > 0;
    consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,Def2;
     reconsider k = m1 as Nat;
    take k;
    now
      let n be Nat;
      dist((seq.n) , g) >= 0 by BHSP_1:37;
      then
A4:   |.(dist((seq.n) , g) - 0).| = dist((seq.n) , g) by ABSVALUE:def 1;
      assume n >= k;
      then dist((seq.n) , g) < r by A3;
      hence |.(dist(seq, g).n - 0).| < r by A4,Def4;
    end;
    hence for n being Nat st k <= n holds |.(dist(seq, g).n - 0).| < r;
  end;
  hence thesis by SEQ_2:def 6;
end;

theorem Th24:
  seq is convergent & lim seq = g implies dist(seq, g) is
  convergent & lim dist(seq, g) = 0
proof
  assume
A1: seq is convergent & lim seq = g;
A2: now
    let r be Real;
    assume
A3: r > 0;
    consider m1 such that
A4: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A3,Def2;
     reconsider k = m1 as Nat;
    take k;
    let n be Nat;
    dist((seq.n) , g) >= 0 by BHSP_1:37;
    then
A5: |.(dist((seq.n) , g) - 0).| = dist((seq.n) , g) by ABSVALUE:def 1;
    assume n >= k;
    then dist((seq.n) , g) < r by A4;
    hence |.(dist(seq, g).n - 0).| < r by A5,Def4;
  end;
  dist(seq, g) is convergent by A1,Th23;
  hence thesis by A2,SEQ_2:def 7;
end;

theorem
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.seq1 + seq2.|| is convergent & lim ||.seq1 + seq2.|| = ||.g1 + g2
  .||
proof
  assume
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
  then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
  hence thesis by Th21;
end;

theorem
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.(seq1 + seq2) - (g1 + g2).|| is convergent & lim ||.(seq1 + seq2)
  - (g1 + g2).|| = 0
proof
  assume
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
  then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
  hence thesis by Th22;
end;

theorem
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.seq1 - seq2.|| is convergent & lim ||.seq1 - seq2.|| = ||.g1 - g2
  .||
proof
  assume
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
  then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
  hence thesis by Th21;
end;

theorem
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.(seq1 - seq2) - (g1 - g2).|| is convergent & lim ||.(seq1 - seq2)
  - (g1 - g2).|| = 0
proof
  assume
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
  then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
  hence thesis by Th22;
end;

theorem
  seq is convergent & lim seq = g implies ||.a * seq.|| is convergent &
  lim ||.a * seq.|| = ||.a * g.||
proof
  assume seq is convergent & lim seq = g;
  then a * seq is convergent & lim (a * seq) = a * g by Th5,Th15;
  hence thesis by Th21;
end;

theorem
  seq is convergent & lim seq = g implies ||.(a * seq) - (a * g).|| is
  convergent & lim ||.(a * seq) - (a * g).|| = 0
proof
  assume seq is convergent & lim seq = g;
  then a * seq is convergent & lim (a * seq) = a * g by Th5,Th15;
  hence thesis by Th22;
end;

theorem
  seq is convergent & lim seq = g implies ||.- seq.|| is convergent &
  lim ||.- seq.|| = ||.- g.||
proof
  assume seq is convergent & lim seq = g;
  then - seq is convergent & lim (- seq) = - g by Th6,Th16;
  hence thesis by Th21;
end;

theorem
  seq is convergent & lim seq = g implies ||.(- seq) - (- g).|| is
  convergent & lim ||.(- seq) - (- g).|| = 0
proof
  assume seq is convergent & lim seq = g;
  then - seq is convergent & lim (- seq) = - g by Th6,Th16;
  hence thesis by Th22;
end;

Lm1: seq is convergent & lim seq = g implies ||.seq + x.|| is convergent & lim
||.seq + x.|| = ||.g + x.||
proof
  assume seq is convergent & lim seq = g;
  then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
  hence thesis by Th21;
end;

theorem Th33:
  seq is convergent & lim seq = g implies ||.(seq + x) - (g + x)
  .|| is convergent & lim ||.(seq + x) - (g + x).|| = 0
proof
  assume seq is convergent & lim seq = g;
  then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
  hence thesis by Th22;
end;

theorem
  seq is convergent & lim seq = g implies ||.seq - x.|| is convergent &
  lim ||.seq - x.|| = ||.g - x.||
proof
  assume
A1: seq is convergent & lim seq = g;
  then lim ||.seq + (-x).|| = ||.g + (-x).|| by Lm1;
  then
A2: lim ||.seq - x.|| = ||.g + (-x).|| by BHSP_1:56;
  ||.seq + (-x).|| is convergent by A1,Lm1;
  hence thesis by A2,BHSP_1:56,RLVECT_1:def 11;
end;

theorem
  seq is convergent & lim seq = g implies ||.(seq - x) - (g - x).|| is
  convergent & lim ||.(seq - x) - (g - x).|| = 0
proof
  assume
A1: seq is convergent & lim seq = g;
  then lim ||.(seq + (-x)) - (g + (-x)).|| = 0 by Th33;
  then
A2: lim ||.(seq - x) - (g + (-x)).|| = 0 by BHSP_1:56;
  ||.(seq + (-x)) - (g + (-x)).|| is convergent by A1,Th33;
  then ||.(seq - x) - (g + (-x)).|| is convergent by BHSP_1:56;
  hence thesis by A2,RLVECT_1:def 11;
end;

theorem
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
  g2 implies dist((seq1 + seq2) , (g1 + g2)) is convergent & lim dist((seq1 +
  seq2) , (g1 + g2)) = 0
proof
  assume
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
  then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
  hence thesis by Th24;
end;

theorem
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
  g2 implies dist((seq1 - seq2) , (g1 - g2)) is convergent & lim dist((seq1 -
  seq2) , (g1 - g2)) = 0
proof
  assume
  seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
  then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
  hence thesis by Th24;
end;

theorem
  seq is convergent & lim seq = g implies dist((a * seq) , (a * g)) is
  convergent & lim dist((a * seq) , (a * g)) = 0
proof
  assume seq is convergent & lim seq = g;
  then a * seq is convergent & lim (a * seq) = a * g by Th5,Th15;
  hence thesis by Th24;
end;

theorem
  seq is convergent & lim seq = g implies dist((seq + x) , (g + x)) is
  convergent & lim dist((seq + x) , (g + x)) = 0
proof
  assume seq is convergent & lim seq = g;
  then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
  hence thesis by Th24;
end;

definition
  let X, x, r;
  func Ball(x,r) -> Subset of X equals
  {y where y is Point of X : ||.x - y.||
  < r};
  coherence
  proof
    defpred P[Point of X] means ||.x - $1.|| < r;
    {y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
    10;
    hence thesis;
  end;
  func cl_Ball(x,r) -> Subset of X equals
  {y where y is Point of X : ||.x - y
  .|| <= r};
  coherence
  proof
    defpred P[Point of X] means ||.x - $1.|| <= r;
    {y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
    10;
    hence thesis;
  end;
  func Sphere(x,r) -> Subset of X equals
  {y where y is Point of X : ||.x - y
  .|| = r};
  coherence
  proof
    defpred P[Point of X] means ||.x - $1.|| = r;
    {y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
    10;
    hence thesis;
  end;
end;

theorem Th40:
  z in Ball(x,r) iff ||.x - z.|| < r
proof
  thus z in Ball(x,r) implies ||.x - z.|| < r
  proof
    assume z in Ball(x,r);
    then ex y be Point of X st z = y & ||.x - y.|| < r;
    hence thesis;
  end;
  thus thesis;
end;

theorem Th41:
  z in Ball(x,r) iff dist(x,z) < r
proof
  thus z in Ball(x,r) implies dist(x,z) < r
  proof
    assume z in Ball(x,r);
    then ||.x - z.|| < r by Th40;
    hence thesis by BHSP_1:def 5;
  end;
  assume dist(x,z) < r;
  then ||.x - z.|| < r by BHSP_1:def 5;
  hence thesis;
end;

theorem
  r > 0 implies x in Ball(x,r)
proof
A1: dist(x,x) = 0 by BHSP_1:34;
  assume r > 0;
  hence thesis by A1,Th41;
end;

theorem
  y in Ball(x,r) & z in Ball(x,r) implies dist(y,z) < 2 * r
proof
  assume that
A1: y in Ball(x,r) and
A2: z in Ball(x,r);
  dist(x,z) < r by A2,Th41;
  then
A3: r + dist(x,z) < r + r by XREAL_1:6;
A4: dist(y,z) <= dist(y,x) + dist(x,z) by BHSP_1:35;
  dist(x,y) < r by A1,Th41;
  then dist(x,y) + dist(x,z) < r + dist(x,z) by XREAL_1:6;
  then dist(x,y) + dist(x,z) < 2 * r by A3,XXREAL_0:2;
  hence thesis by A4,XXREAL_0:2;
end;

theorem
  y in Ball(x,r) implies y - z in Ball(x - z,r)
proof
  assume y in Ball(x,r);
  then
A1: dist(x,y) < r by Th41;
  dist(x - z,y - z) = dist(x,y) by BHSP_1:42;
  hence thesis by A1,Th41;
end;

theorem
  y in Ball(x,r) implies (y - x) in Ball (0.(X),r)
proof
  assume y in Ball(x,r);
  then ||.x - y.|| < r by Th40;
  then ||.(-y) + x.|| < r by RLVECT_1:def 11;
  then ||.-(y - x).|| < r by RLVECT_1:33;
  then ||.09(X) - (y - x).|| < r by RLVECT_1:14;
  hence thesis;
end;

theorem
  y in Ball(x,r) & r <= q implies y in Ball(x,q)
proof
  assume that
A1: y in Ball(x,r) and
A2: r <= q;
  ||.x - y.|| < r by A1,Th40;
  then ||.x - y.|| < q by A2,XXREAL_0:2;
  hence thesis;
end;

theorem Th47:
  z in cl_Ball(x,r) iff ||.x - z.|| <= r
proof
  thus z in cl_Ball(x,r) implies ||.x - z.|| <= r
  proof
    assume z in cl_Ball(x,r);
    then ex y be Point of X st z = y & ||.x - y.|| <= r;
    hence thesis;
  end;
  assume ||.x - z.|| <= r;
  hence thesis;
end;

theorem Th48:
  z in cl_Ball(x,r) iff dist(x,z) <= r
proof
  thus z in cl_Ball(x,r) implies dist(x,z) <= r
  proof
    assume z in cl_Ball(x,r);
    then ||.x - z.|| <= r by Th47;
    hence thesis by BHSP_1:def 5;
  end;
  assume dist(x,z) <= r;
  then ||.x - z.|| <= r by BHSP_1:def 5;
  hence thesis;
end;

theorem
  r >= 0 implies x in cl_Ball(x,r)
proof
  assume r >= 0;
  then dist(x,x) <= r by BHSP_1:34;
  hence thesis by Th48;
end;

theorem Th50:
  y in Ball(x,r) implies y in cl_Ball(x,r)
proof
  assume y in Ball(x,r);
  then ||.x - y.|| <= r by Th40;
  hence thesis;
end;

theorem Th51:
  z in Sphere(x,r) iff ||.x - z.|| = r
proof
  thus z in Sphere(x,r) implies ||.x - z.|| = r
  proof
    assume z in Sphere(x,r);
    then ex y be Point of X st z = y & ||.x - y.|| = r;
    hence thesis;
  end;
  assume ||.x - z.|| = r;
  hence thesis;
end;

theorem
  z in Sphere(x,r) iff dist(x,z) = r
proof
  thus z in Sphere(x,r) implies dist(x,z) = r
  proof
    assume z in Sphere(x,r);
    then ||.x - z.|| = r by Th51;
    hence thesis by BHSP_1:def 5;
  end;
  assume dist(x,z) = r;
  then ||.x - z.|| = r by BHSP_1:def 5;
  hence thesis;
end;

theorem
  y in Sphere(x,r) implies y in cl_Ball(x,r)
proof
  assume y in Sphere(x,r);
  then ||.x - y.|| = r by Th51;
  hence thesis;
end;

theorem Th54:
  Ball(x,r) c= cl_Ball(x,r)
proof
  for y holds y in Ball(x,r) implies y in cl_Ball(x,r) by Th50;
  hence thesis by SUBSET_1:2;
end;

theorem Th55:
  Sphere(x,r) c= cl_Ball(x,r)
proof
  now
    let y;
    assume y in Sphere(x,r);
    then ||.x - y.|| = r by Th51;
    hence y in cl_Ball(x,r);
  end;
  hence thesis by SUBSET_1:2;
end;

theorem
  Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r)
proof
  now
    let y;
    assume y in cl_Ball(x,r);
    then
A1: ||.x - y.|| <= r by Th47;
    now
      per cases by A1,XXREAL_0:1;
      case
        ||.x - y.|| < r;
        hence y in Ball(x,r);
      end;
      case
        ||.x - y.|| = r;
        hence y in Sphere(x,r);
      end;
    end;
    hence y in Ball(x,r) \/ Sphere(x,r) by XBOOLE_0:def 3;
  end;
  then
A2: cl_Ball(x,r) c= Ball(x,r) \/ Sphere(x,r) by SUBSET_1:2;
  Ball(x,r) c= cl_Ball(x,r) & Sphere(x,r) c= cl_Ball(x,r) by Th54,Th55;
  then Ball(x,r) \/ Sphere(x,r) c= cl_Ball(x,r) by XBOOLE_1:8;
  hence thesis by A2,XBOOLE_0:def 10;
end;