:: On Some Properties of Real {H}ilbert Space, {II}
::  by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama
::
:: Received April 17, 2003
:: Copyright (c) 2003-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, BHSP_1, PRE_TOPC, REAL_1, COMPLEX1, ARYTM_1, ARYTM_3,
      XXREAL_0, XREAL_0, ORDINAL1, CARD_1, SUBSET_1, RELAT_1, HAHNBAN, BHSP_6,
      FINSET_1, XBOOLE_0, TARSKI, BHSP_5, STRUCT_0, BINOP_2, FUNCT_1, ZFMISC_1,
      NAT_1, SEQ_2, ALGSTR_0, BINOP_1, SETWISEO, PROB_2, FINSEQ_1, FINSOP_1,
      SQUARE_1, NORMSP_1, SEMI_AF1, SUPINF_2, RSSPACE2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0,
      BINOP_2, STRUCT_0, ALGSTR_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2,
      RELAT_1, PRE_TOPC, BHSP_1, SQUARE_1, SEQ_2, BINOP_1, FINSET_1, SETWISEO,
      HAHNBAN, FINSEQ_1, FINSOP_1, BHSP_5, BHSP_6, RSSPACE2, PARTFUN1,
      XXREAL_0;
 constructors BINOP_1, DOMAIN_1, SETWISEO, REAL_1, SQUARE_1, BINOP_2, COMPLEX1,
      FINSOP_1, BHSP_3, BHSP_5, BHSP_6, SEQ_1, RELSET_1, COMSEQ_2;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1,
      NUMBERS, XREAL_0, BINOP_2, STRUCT_0, BHSP_5;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, SQUARE_1, RLVECT_1;
 theorems XBOOLE_1, SQUARE_1, ZFMISC_1, XREAL_0, ABSVALUE, FUNCT_1, NAT_1,
      FUNCT_2, RLVECT_1, SEQ_2, SEQ_4, BHSP_1, BHSP_5, BHSP_6, UNIFORM1,
      CHAIN_1, XCMPLX_1, BINOP_2, XREAL_1, COMPLEX1, XXREAL_0;
 schemes NAT_1, FUNCT_2;

begin :: Necessary and sufficient condition for summable set

reserve X for RealUnitarySpace;
reserve x, y, y1, y2 for Point of X;

Lm1: for x, y, z, e be Real holds abs(x-y) < e/2 & abs(y-z) < e/2 implies abs(
x-z) <e
proof
  let x, y, z, e be Real;
  assume abs(x-y) < e/2 & abs(y-z) <e/2;
  then abs((x-y)+(y-z)) <= abs(x-y)+abs(y-z) & abs(x-y)+abs(y-z) < e/2+e/2 by
COMPLEX1:56,XREAL_1:8;
  hence thesis by XXREAL_0:2;
end;

Lm2: for p being real number st p > 0 ex k be Element of NAT st 1/(k+1) < p
proof
  let p be real number;
  consider k1 be Element of NAT such that
A1: p" < k1 by SEQ_4:3;
  assume p > 0;
  then
A2: 0 < p" by XREAL_1:122;
  take k1;
  p"+0 < k1+1 by A1,XREAL_1:8;
  then 1/(k1+1) < 1/p" by A2,XREAL_1:76;
  hence thesis by XCMPLX_1:216;
end;

Lm3: for p being real number, m being Element of NAT st p > 0 ex i be Element
of NAT st 1/(i+1) < p & i >= m
proof
  let p be real number, m be Element of NAT;
  consider k1 be Element of NAT such that
A1: p"<k1 by SEQ_4:3;
  assume p > 0;
  then
A2: 0<p" by XREAL_1:122;
  take i = k1+m;
  k1 <= k1 + m by NAT_1:11;
  then p" < i by A1,XXREAL_0:2;
  then p"+0 < i+1 by XREAL_1:8;
  then 1/(i+1) < 1/p" by A2,XREAL_1:76;
  hence thesis by NAT_1:11,XCMPLX_1:216;
end;

theorem Th1:
  for Y be Subset of X for L be Functional of X holds Y
is_summable_set_by L iff for e be Real st 0 < e holds ex Y0 be finite Subset of
  X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non
empty & Y1 c= Y & Y0 misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL,
  L, addreal)) <e
proof
  let Y be Subset of X;
  let L be Functional of X;
  thus Y is_summable_set_by L implies for e be Real st 0 < e holds ex Y0 be
finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X
st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds abs(setopfunc(Y1, the carrier
  of X, REAL, L, addreal)) <e
  proof
    assume Y is_summable_set_by L;
    then consider r be Real such that
A1: for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(
    r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e by BHSP_6:def 6;
    for e be Real st 0 < e holds ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y &
Y0 misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)) <e
    proof
      let e be Real;
      assume 0 < e;
      then consider Y0 be finite Subset of X such that
A2:   Y0 is non empty and
A3:   Y0 c= Y and
A4:   for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(r -
setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e/2 by A1,XREAL_1:139;
      for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0
misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e
      proof
        let Y1 be finite Subset of X such that
        Y1 is non empty and
A5:     Y1 c= Y and
A6:     Y0 misses Y1;
        set Y19 = Y0 \/ Y1;
        dom L = the carrier of X by FUNCT_2:def 1;
        then setopfunc(Y19, the carrier of X, REAL, L, addreal) = addreal.(
setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y1, the carrier of
        X, REAL, L, addreal)) by A6,BHSP_5:14
          .= setopfunc(Y0, the carrier of X, REAL, L, addreal) + setopfunc(
        Y1, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
        then
A7:     setopfunc(Y1, the carrier of X, REAL, L, addreal) = setopfunc(Y19
, the carrier of X, REAL, L, addreal) - setopfunc(Y0, the carrier of X, REAL, L
        , addreal);
        Y0 c= Y19 by XBOOLE_1:7;
        then
        abs(r - setopfunc(Y19, the carrier of X, REAL, L, addreal)) < e/2
        by A3,A4,A5,XBOOLE_1:8;
        then
A8:     abs(setopfunc(Y19, the carrier of X, REAL, L, addreal)-r) < e/2
        by UNIFORM1:11;
        abs(r - setopfunc(Y0, the carrier of X, REAL, L, addreal)) < e/2
        by A3,A4;
        hence thesis by A8,A7,Lm1;
      end;
      hence thesis by A2,A3;
    end;
    hence thesis;
  end;
  assume
A9: for e be Real st 0 < e holds ex Y0 be finite Subset of X st Y0 is
non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y
& Y0 misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)) <e;
  ex r be Real st for e be Real st 0 < e ex Y0 be finite Subset of X st
Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
  holds abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e
  proof
    defpred P[set,set] means $2 is finite Subset of X & $2 is non empty & $2
c= Y & for z be Real st z=$1 for Y1 be finite Subset of X st Y1 is non empty &
    Y1 c= Y & $2 misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L,
    addreal)) < 1/(z+1);
    now
      let x be set;
      assume x in NAT;
      then reconsider xx = x as Element of NAT;
      reconsider e = 1/(xx+1) as Real;
      0 <= xx by NAT_1:2;
      then 0 < xx + 1 by NAT_1:13;
      then 0/(xx + 1) < 1/(xx + 1) by XREAL_1:74;
      then consider Y0 be finite Subset of X such that
A10:  Y0 is non empty and
A11:  Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1
c= Y & Y0 misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)
      ) < e by A9;
      Y0 in bool Y & for z be Real st z = x for Y1 be finite Subset of X
st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds abs(setopfunc(Y1, the carrier
      of X, REAL, L, addreal)) < 1/(z+1) by A11,ZFMISC_1:def 1;
      hence ex y be set st y in bool Y & y is finite Subset of X & y is non
empty & y c= Y & for z be Real st z=x for Y1 be finite Subset of X st Y1 is non
empty & Y1 c= Y & y misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L
      , addreal)) < 1/(z+1) by A10;
    end;
    then
A12: for x be set st x in NAT ex y be set st y in bool Y & P[x,y];
A13: ex B being Function of NAT,bool Y st for x be set st x in NAT holds P
    [x,B. x] from FUNCT_2:sch 1(A12);
    ex A be Function of NAT, bool Y st for i be Element of NAT holds A.i
is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset
of X st Y1 is non empty & Y1 c= Y & A.i misses Y1 holds abs(setopfunc(Y1, the
carrier of X, REAL, L, addreal)) < 1/(i+1)) & for j be Element of NAT st i <= j
    holds A.i c= A.j
    proof
      consider B being Function of NAT,bool Y such that
A14:  for x be set st x in NAT holds B.x is finite Subset of X & B.x
is non empty & B.x c= Y & for z be Real st z=x for Y1 be finite Subset of X st
Y1 is non empty & Y1 c= Y & B.x misses Y1 holds abs(setopfunc(Y1, the carrier
      of X, REAL, L, addreal)) < 1/(z+1) by A13;
      deffunc G(Nat,set) = B.($1+1) \/ $2;
      ex A being Function st dom A = NAT & A.0 = B.0 & for n being Nat
      holds A.(n+1) = G(n,A.n) from NAT_1:sch 11;
      then consider A being Function such that
A15:  dom A = NAT and
A16:  A.0 = B.0 and
A17:  for n being Nat holds A.(n+1) = B.(n+1) \/ A.n;
      defpred R[Element of NAT] means A.$1 is finite Subset of X & A.$1 is non
empty & A.$1 c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y
& A.$1 misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)) <
      1/($1+1)) & for j be Element of NAT st $1 <= j holds A.$1 c= A.j;
A18:  now
        let n be Element of NAT such that
A19:    R[n];
A20:    for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.(n+
1) misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)) < 1/(
        (n+1)+1)
        proof
          let Y1 be finite Subset of X such that
A21:      Y1 is non empty & Y1 c= Y and
A22:      A.(n+1) misses Y1;
          A.(n+1) = B.(n+1) \/ A.n by A17;
          then B.(n+1) misses Y1 by A22,XBOOLE_1:7,63;
          hence thesis by A14,A21;
        end;
        defpred P[Element of NAT] means (n+1) <= $1 implies A.(n+1) c= A.$1;
A23:    for j being Element of NAT st P[j] holds P[j+1]
        proof
          let j be Element of NAT such that
A24:      P[j] and
A25:      n+1 <= j+1;
          now
            per cases;
            case
              n = j;
              hence thesis;
            end;
            case
A26:          n <> j;
              A.(j+1) = (B.(j+1) \/ A.j) by A17;
              then
A27:          A.j c= A.(j+1) by XBOOLE_1:7;
              n <= j by A25,XREAL_1:6;
              then n < j by A26,XXREAL_0:1;
              hence thesis by A24,A27,NAT_1:13,XBOOLE_1:1;
            end;
          end;
          hence thesis;
        end;
A28:    P[0] by NAT_1:3;
A29:    for j be Element of NAT holds P[j] from NAT_1:sch 1(A28, A23);
        A.(n+1) = B.(n+1) \/ A.n & B.(n+1) is finite Subset of X by A14,A17;
        hence R[n+1] by A19,A20,A29,XBOOLE_1:8;
      end;
      for j0 be Element of NAT st j0=0 holds for j be Element of NAT st
      j0 <= j holds A.j0 c= A.j
      proof
        let j0 be Element of NAT such that
A30:    j0 = 0;
        defpred P[Element of NAT] means j0 <= $1 implies A.j0 c= A.$1;
A31:    now
          let j be Element of NAT such that
A32:      P[j];
          A.(j+1) = (B.(j+1) \/ A.j) by A17;
          then A.j c= A.(j+1) by XBOOLE_1:7;
          hence P[j+1] by A30,A32,NAT_1:2,XBOOLE_1:1;
        end;
A33:    P[0] by A30;
        thus for j be Element of NAT holds P[j] from NAT_1:sch 1(A33, A31 );
      end;
      then
A34:  R[0] by A14,A16;
A35:  for i be Element of NAT holds R[i] from NAT_1:sch 1(A34,A18);
      rng A c= bool Y
      proof
        let y be set;
        assume y in rng A;
        then consider x be set such that
A36:    x in dom A and
A37:    y = A.x by FUNCT_1:def 3;
        reconsider i = x as Element of NAT by A15,A36;
        A.i c= Y by A35;
        hence thesis by A37,ZFMISC_1:def 1;
      end;
      then A is Function of NAT, bool Y by A15,FUNCT_2:2;
      hence thesis by A35;
    end;
    then consider A be Function of NAT, bool Y such that
A38: for i be Element of NAT holds A.i is finite Subset of X & A.i is
non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c=
Y & A.i misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal))<
    1/(i+1)) & for j be Element of NAT st i <= j holds A.i c= A.j;
    defpred P[set,set] means ex Y1 be finite Subset of X st Y1 is non empty &
    A.$1 = Y1 & $2 = setopfunc(Y1, the carrier of X, REAL, L, addreal);
A39: for x be set st x in NAT ex y be set st y in REAL & P[x,y]
    proof
      let x be set;
      assume x in NAT;
      then reconsider i=x as Element of NAT;
      A.i is finite Subset of X by A38;
      then reconsider Y1 = A.x as finite Subset of X;
      reconsider y = setopfunc(Y1, the carrier of X, REAL, L, addreal) as set;
      A.i is non empty by A38;
      then ex Y1 be finite Subset of X st Y1 is non empty & A.x = Y1 & y =
      setopfunc(Y1, the carrier of X, REAL, L, addreal);
      hence thesis;
    end;
    ex F being Function of NAT, REAL st for x be set st x in NAT holds P[
    x,F.x] from FUNCT_2:sch 1(A39);
    then consider F being Function of NAT, REAL such that
A40: for x be set st x in NAT holds ex Y1 be finite Subset of X st Y1
    is non empty & A.x = Y1 & F.x = setopfunc(Y1, the carrier of X, REAL, L,
    addreal);
    set seq = F;
A41: for e be real number st e > 0 ex k be Element of NAT st for n, m be
    Element of NAT st n >= k & m >= k holds abs((seq.n) - (seq.m)) < e
    proof
      let e be real number such that
A42:  e > 0;
A43:  e/2 > 0/2 by A42,XREAL_1:74;
      then consider k be Element of NAT such that
A44:  1/(k+1) < e/2 by Lm2;
      take k;
      let n, m be Element of NAT such that
A45:  n >= k and
A46:  m >= k;
      consider Y2 be finite Subset of X such that
      Y2 is non empty and
A47:  A.m = Y2 and
A48:  seq.m = setopfunc(Y2, the carrier of X, REAL, L, addreal) by A40;
      consider Y0 be finite Subset of X such that
      Y0 is non empty and
A49:  A.k = Y0 and
      seq.k = setopfunc(Y0, the carrier of X, REAL, L, addreal) by A40;
A50:  Y0 c= Y2 by A38,A46,A49,A47;
      consider Y1 be finite Subset of X such that
      Y1 is non empty and
A51:  A.n = Y1 and
A52:  seq.n = setopfunc(Y1, the carrier of X, REAL, L, addreal) by A40;
A53:  Y0 c= Y1 by A38,A45,A49,A51;
      now
        per cases;
        case
A54:      Y0 = Y1;
          now
            per cases;
            case
              Y0 = Y2;
              hence thesis by A42,A52,A48,A54,ABSVALUE:2;
            end;
            case
A55:          Y0 <> Y2;
              ex Y02 be finite Subset of X st Y02 is non empty & Y02 c= Y
              & Y02 misses Y0 & Y0 \/ Y02 = Y2
              proof
                take Y02 = Y2 \ Y0;
A56:            Y2 \ Y0 c= Y2 by XBOOLE_1:36;
                Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
                  .= Y2 by A50,XBOOLE_1:12;
                hence thesis by A47,A55,A56,XBOOLE_1:1,79;
              end;
              then consider Y02 be finite Subset of X such that
A57:          Y02 is non empty & Y02 c= Y and
A58:          Y02 misses Y0 and
A59:          Y0 \/ Y02 = Y2;
              abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) <
              1/(k+1) by A38,A49,A57,A58;
              then
A60:          abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) <
              e/2 by A44,XXREAL_0:2;
              dom L = the carrier of X by FUNCT_2:def 1;
              then setopfunc(Y2, the carrier of X, REAL, L, addreal) =
addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y02, the
              carrier of X, REAL, L, addreal)) by A58,A59,BHSP_5:14
                .= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y02, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
              then
A61:          abs((seq.n) - (seq.m)) = abs(-setopfunc(Y02, the carrier
              of X, REAL, L, addreal)) by A52,A48,A54
                .= abs(setopfunc(Y02, the carrier of X, REAL, L, addreal))
              by COMPLEX1:52;
              e/2 < e by A42,XREAL_1:216;
              hence thesis by A60,A61,XXREAL_0:2;
            end;
          end;
          hence thesis;
        end;
        case
A62:      Y0 <> Y1;
          now
            per cases;
            case
A63:          Y0 = Y2;
              ex Y01 be finite Subset of X st Y01 is non empty & Y01 c=
              Y & Y01 misses Y0 & Y0 \/ Y01 = Y1
              proof
                take Y01 = Y1 \ Y0;
A64:            Y1 \ Y0 c= Y1 by XBOOLE_1:36;
                Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
                  .= Y1 by A53,XBOOLE_1:12;
                hence thesis by A51,A62,A64,XBOOLE_1:1,79;
              end;
              then consider Y01 be finite Subset of X such that
A65:          Y01 is non empty & Y01 c= Y and
A66:          Y01 misses Y0 and
A67:          Y0 \/ Y01 = Y1;
              dom L = the carrier of X by FUNCT_2:def 1;
              then
A68:          setopfunc(Y1, the carrier of X, REAL, L, addreal) =
addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y01, the
              carrier of X, REAL, L, addreal)) by A66,A67,BHSP_5:14
                .= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y01, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
              abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) <
              1/(k+1) by A38,A49,A65,A66;
              then
              abs((seq.n) - (seq.m)) < e/2 by A44,A52,A48,A63,A68,XXREAL_0:2;
              then abs((seq.n) - (seq.m))+ 0 < e/2 + e/2 by A43,XREAL_1:8;
              hence thesis;
            end;
            case
A69:          Y0<>Y2;
              ex Y02 be finite Subset of X st Y02 is non empty & Y02 c=
              Y & Y02 misses Y0 & Y0 \/ Y02 = Y2
              proof
                take Y02 = Y2 \ Y0;
A70:            Y2 \ Y0 c= Y2 by XBOOLE_1:36;
                Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
                  .= Y2 by A50,XBOOLE_1:12;
                hence thesis by A47,A69,A70,XBOOLE_1:1,79;
              end;
              then consider Y02 be finite Subset of X such that
A71:          Y02 is non empty & Y02 c= Y and
A72:          Y02 misses Y0 and
A73:          Y0 \/ Y02 = Y2;
              dom L = the carrier of X by FUNCT_2:def 1;
              then
A74:          setopfunc(Y2, the carrier of X, REAL, L, addreal) =
addreal.(setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y02, the
              carrier of X, REAL, L, addreal)) by A72,A73,BHSP_5:14
                .= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y02, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
              ex Y01 be finite Subset of X st Y01 is non empty & Y01 c=
              Y & Y01 misses Y0 & Y0 \/ Y01 = Y1
              proof
                take Y01 = Y1 \ Y0;
A75:            Y1 \ Y0 c= Y1 by XBOOLE_1:36;
                Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
                  .= Y1 by A53,XBOOLE_1:12;
                hence thesis by A51,A62,A75,XBOOLE_1:1,79;
              end;
              then consider Y01 be finite Subset of X such that
A76:          Y01 is non empty & Y01 c= Y and
A77:          Y01 misses Y0 and
A78:          Y0 \/ Y01 = Y1;
              dom L = the carrier of X by FUNCT_2:def 1;
              then setopfunc(Y1, the carrier of X, REAL, L, addreal) =
addreal.(setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y01, the
              carrier of X, REAL, L, addreal)) by A77,A78,BHSP_5:14
                .= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y01, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
              then seq.n - seq.m = setopfunc(Y01, the carrier of X, REAL, L,
addreal) - setopfunc(Y02, the carrier of X, REAL, L, addreal) by A52,A48,A74;
              then
A79:          abs((seq.n) - (seq.m)) <= abs(setopfunc(Y01, the carrier
of X, REAL, L, addreal)) + abs(setopfunc(Y02, the carrier of X, REAL, L,
              addreal)) by COMPLEX1:57;
              abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) <
              1/(k+1) by A38,A49,A71,A72;
              then
A80:          abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) <
              e/2 by A44,XXREAL_0:2;
              abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) <
              1/(k+1) by A38,A49,A76,A77;
              then abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) <
              e/2 by A44,XXREAL_0:2;
              then abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) +
abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) < e/2 + e/2 by A80,
XREAL_1:8;
              hence thesis by A79,XXREAL_0:2;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    for e be real number st 0 < e ex k be Element of NAT st for m be
    Element of NAT st k <= m holds abs(seq.m -seq.k)<e
    proof
      let e be real number;
      assume 0 < e;
      then consider k be Element of NAT such that
A81:  for n, m be Element of NAT st n >= k & m >= k holds abs((seq.n
      ) - (seq.m)) < e by A41;
      for m be Element of NAT st k <= m holds abs(seq.m - seq.k)<e by A81;
      hence thesis;
    end;
    then seq is convergent by SEQ_4:41;
    then consider x be real number such that
A82: for r be real number st r > 0 ex m be Element of NAT st for n be
    Element of NAT st n >= m holds abs(seq.n - x) < r by SEQ_2:def 6;
    reconsider r=x as Real by XREAL_0:def 1;
    take r;
    for e be Real st 0 < e ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(
    r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e
    proof
      let e be Real;
      assume e > 0;
      then
A83:  e/2 > 0/2 by XREAL_1:74;
      then consider m be Element of NAT such that
A84:  for n be Element of NAT st n >= m holds abs((seq.n)-r) < e/2 by A82;
      consider i be Element of NAT such that
A85:  1/(i+1) < e/2 and
A86:  i >= m by A83,Lm3;
      consider Y0 be finite Subset of X such that
A87:  Y0 is non empty and
A88:  A.i = Y0 and
A89:  seq.i = setopfunc(Y0, the carrier of X, REAL, L, addreal) by A40;
A90:  abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) < e/2
      by A84,A86,A89;
      now
        let Y1 be finite Subset of X such that
A91:    Y0 c= Y1 and
A92:    Y1 c= Y;
        now
          per cases;
          case
            Y0 = Y1;
            then abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) <
            e/2 by A90,UNIFORM1:11;
            then abs(x - setopfunc(Y1, the carrier of X, REAL, L, addreal)) +
            0 < e/2 + e/2 by A83,XREAL_1:8;
            hence abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) <
            e;
          end;
          case
A93:        Y0 <> Y1;
            ex Y2 be finite Subset of X st Y2 is non empty & Y2 c= Y &
            Y0 misses Y2 & Y0 \/ Y2 = Y1
            proof
              take Y2 = Y1 \ Y0;
A94:          Y1 \ Y0 c= Y1 by XBOOLE_1:36;
              Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
                .= Y1 by A91,XBOOLE_1:12;
              hence thesis by A92,A93,A94,XBOOLE_1:1,79;
            end;
            then consider Y2 be finite Subset of X such that
A95:        Y2 is non empty & Y2 c= Y and
A96:        Y0 misses Y2 and
A97:        Y0 \/ Y2 = Y1;
            dom L = the carrier of X by FUNCT_2:def 1;
            then setopfunc(Y1, the carrier of X, REAL, L, addreal)-r =
addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y2, the
            carrier of X, REAL, L, addreal)) - r by A96,A97,BHSP_5:14
              .= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y2, the carrier of X, REAL, L, addreal) - r by BINOP_2:def 9
              .= setopfunc(Y0, the carrier of X, REAL, L, addreal) - r +
            setopfunc(Y2, the carrier of X, REAL, L, addreal);
            then abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)-r) <=
abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) + abs(setopfunc(Y2,
            the carrier of X, REAL, L, addreal)) by ABSVALUE:9;
            then
A98:        abs(x - setopfunc(Y1, the carrier of X, REAL, L, addreal) )
<= abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) + abs(setopfunc(
            Y2, the carrier of X, REAL, L, addreal)) by UNIFORM1:11;
            abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) < 1/(
            i+1) by A38,A88,A95,A96;
            then abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) < e/2
            by A85,XXREAL_0:2;
            then abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) +
abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) < e/2 + e/2 by A90,
XREAL_1:8;
            hence abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) <
            e by A98,XXREAL_0:2;
          end;
        end;
        hence abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e;
      end;
      hence thesis by A87,A88;
    end;
    hence thesis;
  end;
  hence thesis by BHSP_6:def 6;
end;

theorem Th2:
  for X st the addF of X is commutative associative & the addF of X
is having_a_unity for S be finite OrthogonalFamily of X st S is non empty for I
  be Function of the carrier of X, the carrier of X st S c= dom I & (for y st y
in S holds I.y = y) for H be Function of the carrier of X, REAL st S c= dom H &
  (for y st y in S holds H.y= (y.|.y)) holds setopfunc(S, the carrier of X, the
carrier of X, I, the addF of X) .|. setopfunc(S, the carrier of X, the carrier
  of X, I, the addF of X) = setopfunc(S, the carrier of X, REAL, H, addreal)
proof
  let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
  let S be finite OrthogonalFamily of X such that
A2: S is non empty;
  let I be Function of the carrier of X, the carrier of X such that
A3: S c= dom I and
A4: for y st y in S holds I.y = y;
  consider p be FinSequence of the carrier of X such that
A5: p is one-to-one & rng p = S and
A6: setopfunc(S, (the carrier of X), (the carrier of X), I, (the addF of
  X)) = (the addF of X) "**" Func_Seq(I, p) by A1,A3,BHSP_5:def 5;
  let H be Function of the carrier of X, REAL such that
A7: S c= dom H and
A8: for y st y in S holds H.y= y.|.y;
A9: setopfunc(S, the carrier of X, REAL, H, addreal) = addreal "**" Func_Seq
  (H, p) by A7,A5,BHSP_5:def 5;
A10: for y1, y2 st y1 in S & y2 in S & y1 <> y2 holds (the scalar of X).[I.
  y1, I.y2] = 0
  proof
    let y1, y2;
    assume that
A11: y1 in S & y2 in S and
A12: y1 <> y2;
A13: y1.|.y2 = 0 by A11,A12,BHSP_5:def 8;
    I.y1 = y1 & I.y2 = y2 by A4,A11;
    hence thesis by A13,BHSP_1:def 1;
  end;
  for y st y in S holds H.y = (the scalar of X).[I.y, I.y]
  proof
    let y;
    assume
A14: y in S;
    then
A15: I.y = y by A4;
    H.y = (y.|.y) by A8,A14
      .= (the scalar of X).[I.y, I.y] by A15,BHSP_1:def 1;
    hence thesis;
  end;
  then
  (the scalar of X).[(the addF of X) "**" Func_Seq(I, p), (the addF of X)
  "**" Func_Seq(I, p)] = addreal "**" Func_Seq(H, p) by A2,A3,A7,A5,A10,
BHSP_5:9;
  hence thesis by A6,A9,BHSP_1:def 1;
end;

theorem Th3:
  for X st the addF of X is commutative associative & the addF of X
is having_a_unity for S be finite OrthogonalFamily of X st S is non empty for H
be Functional of X st S c= dom H & (for x st x in S holds H.x = (x.|.x)) holds
  (setsum(S)).|.(setsum(S)) = setopfunc(S, the carrier of X, REAL, H, addreal)
proof
  let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
  reconsider I = id the carrier of X as Function of the carrier of X, the
  carrier of X;
  let S be finite OrthogonalFamily of X such that
A2: S is non empty;
  let H be Functional of X such that
A3: S c= dom H & for x st x in S holds H.x = (x.|.x);
A4: for x st x in S holds I.x = x by FUNCT_1:18;
A5: dom I = the carrier of X by FUNCT_2:def 1;
  for x be set st x in the carrier of X holds I.x = x by FUNCT_1:18;
  then
  setsum(S) = setopfunc(S, the carrier of X, the carrier of X, I, the addF
  of X) by A1,A5,BHSP_6:1;
  hence thesis by A1,A2,A3,A5,A4,Th2;
end;

theorem Th4:
  for Y be OrthogonalFamily of X for Z be Subset of X holds Z is
  Subset of Y implies Z is OrthogonalFamily of X
proof
  let Y be OrthogonalFamily of X;
  let Z be Subset of X;
  assume Z is Subset of Y;
  then for x, y st x in Z & y in Z & x <> y holds x.|.y = 0 by BHSP_5:def 8;
  hence thesis by BHSP_5:def 8;
end;

theorem Th5:
  for Y be OrthonormalFamily of X for Z be Subset of X holds Z is
  Subset of Y implies Z is OrthonormalFamily of X
proof
  let Y be OrthonormalFamily of X;
  let Z be Subset of X;
  assume
A1: Z is Subset of Y;
  then
A2: for x st x in Z holds x.|.x = 1 by BHSP_5:def 9;
  Y is OrthogonalFamily of X by BHSP_5:def 9;
  then Z is OrthogonalFamily of X by A1,Th4;
  hence thesis by A2,BHSP_5:def 9;
end;

begin :: Equivalence of summability

theorem Th6:
  for X being RealHilbertSpace
   st the addF of X is commutative associative & the addF of X
  is having_a_unity for S be OrthonormalFamily of X for H be
  Functional of X st S c= dom H &
   (for x being Point of X st x in S holds H.x = (x.|.x)) holds S
  is summable_set iff S is_summable_set_by H
proof
  let X be RealHilbertSpace such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
  let S be OrthonormalFamily of X;
  let H be Functional of X such that
A2: S c= dom H and
A3: for x being Point of X st x in S holds H.x = (x.|.x);
A4: now
    assume
A5: S is summable_set;
    now
      let e be Real such that
A6:   0 < e;
      set e9 = sqrt e;
      0 < e9 by A6,SQUARE_1:25;
      then consider e1 be Real such that
A7:   0 < e1 and
A8:   e1 < e9 by CHAIN_1:1;
      e1^2 < e9^2 by A7,A8,SQUARE_1:16;
      then
A9:  e1*e1 < e by A6,SQUARE_1:def 2;
      consider Y0 be finite Subset of X such that
A10:  Y0 is non empty & Y0 c= S and
A11:  for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S & Y0
      misses Y1 holds ||.setsum(Y1).|| < e1 by A1,A5,A7,BHSP_6:10;
      take Y0;
      thus Y0 is non empty & Y0 c= S by A10;
      let Y1 be finite Subset of X such that
A12:  Y1 is non empty and
A13:  Y1 c= S and
A14:  Y0 misses Y1;
      Y1 is finite OrthonormalFamily of X by A13,Th5;
      then
A15:  Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
      for x being Point of X st x in Y1 holds H.x = (x.|.x) by A3,A13;
      then
A16:  (setsum(Y1)).|.(setsum(Y1)) = setopfunc(Y1, the carrier of X, REAL,
      H, addreal) by A1,A2,A12,A13,A15,Th3,XBOOLE_1:1;
      0 <= ||.setsum(Y1).|| by BHSP_1:28;
      then ||.setsum(Y1).||^2 < e1^2 by A11,A12,A13,A14,SQUARE_1:16;
      then
A17:  ||.setsum(Y1).||^2 < e by A9,XXREAL_0:2;
      ||.setsum(Y1).|| = sqrt ((setsum(Y1)).|.(setsum(Y1))) & 0 <= (
      setsum(Y1)).|. (setsum(Y1)) by BHSP_1:def 2,def 4;
      then
A18:  ||.setsum(Y1).||^2 = setopfunc(Y1, the carrier of X, REAL, H,
      addreal) by A16,SQUARE_1:def 2;
      0 <= setopfunc(Y1, the carrier of X, REAL, H, addreal) by A16,
BHSP_1:def 2;
      hence abs(setopfunc(Y1, the carrier of X, REAL, H, addreal)) < e by A17
,A18,ABSVALUE:def 1;
    end;
    hence S is_summable_set_by H by Th1;
  end;
  now
    assume
A19: S is_summable_set_by H;
    now
      let e be Real such that
A20:  0 < e;
      set e1 = e * e;
      0 < e1 by A20,XREAL_1:129;
      then consider Y0 be finite Subset of X such that
A21:  Y0 is non empty & Y0 c= S and
A22:  for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S & Y0
misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, H, addreal)) < e1 by
A19,Th1;
      now
        let Y1 be finite Subset of X such that
A23:    Y1 is non empty and
A24:    Y1 c= S and
A25:    Y0 misses Y1;
        set F = setopfunc(Y1, the carrier of X, REAL, H, addreal);
        Y1 is finite OrthonormalFamily of X by A24,Th5;
        then
A26:    Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
        abs F < e1 by A22,A23,A24,A25;
        then F - e1 < abs F - abs F by ABSVALUE:4,XREAL_1:15;
        then
A27:    F < e1 by XREAL_1:48;
        for x being Point of X st x in Y1 holds H.x= (x.|.x) by A3,A24;
        then
A28:    (setsum Y1).|.(setsum Y1) = F by A1,A2,A23,A24,A26,Th3,XBOOLE_1:1;
        0 <= (setsum Y1).|.(setsum Y1) & ||.setsum Y1.|| = sqrt ((setsum
        Y1).|.( setsum Y1)) by BHSP_1:def 2,def 4;
        then ||.setsum Y1.||^2 < e1 by A27,A28,SQUARE_1:def 2;
        then sqrt(||.setsum(Y1).||^2) < sqrt(e^2) by SQUARE_1:27,XREAL_1:63;
        then sqrt(||.setsum(Y1).||^2) < e by A20,SQUARE_1:22;
        hence ||.setsum(Y1).|| < e by BHSP_1:28,SQUARE_1:22;
      end;
      hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= S & for Y1
be finite Subset of X st Y1 is non empty & Y1 c= S & Y0 misses Y1 holds ||.
      setsum(Y1).|| < e by A21;
    end;
    hence S is summable_set by A1,BHSP_6:10;
  end;
  hence thesis by A4;
end;

theorem Th7:
  for S be Subset of X st S is summable_set holds for e be Real st
  0 < e ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= S & for Y1 be
  finite Subset of X st Y0 c= Y1 & Y1 c= S holds abs(((sum(S)).|.(sum(S))) - ((
  setsum(Y1)).|.(setsum(Y1)))) < e
proof
  let S be Subset of X such that
A1: S is summable_set;
  consider Y02 be finite Subset of X such that
  Y02 is non empty and
A2: Y02 c= S and
A3: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= S holds ||.sum(S)
  - setsum(Y1).|| < 1 by A1,BHSP_6:def 3;
  let e be Real such that
A4: 0 < e;
  set e9 = e/(2*||.sum(S).||+1);
  0 <= ||.sum(S).|| by BHSP_1:28;
  then 0 <= 2*||.sum(S).|| by XREAL_1:127;
  then
A5: 0+0 < 2*||.sum(S).||+1 by XREAL_1:8;
  then 0 < e9 by A4,XREAL_1:139;
  then consider Y01 be finite Subset of X such that
A6: Y01 is non empty and
A7: Y01 c= S and
A8: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= S holds ||.sum(S)
  - setsum(Y1).|| < e9 by A1,BHSP_6:def 3;
  set Y0 = Y01 \/ Y02;
A9: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= S holds abs(((sum(S))
  .|.(sum(S))) - ((setsum(Y1)).|.(setsum(Y1)))) < e
  proof
    let Y1 be finite Subset of X such that
A10: Y0 c= Y1 and
A11: Y1 c= S;
    set SS = sum(S)-setsum(Y1), SY = setsum(Y1);
    Y01 c= Y1 by A10,XBOOLE_1:11;
    then
A12: ||.SS.||*(2*||.sum(S).|| + 1) < e9*(2*||.sum(S).|| + 1) by A5,A8,A11,
XREAL_1:68;
    ||.SY.|| = ||.-SY.|| by BHSP_1:31
      .= ||.0.X - SY.|| by RLVECT_1:14
      .= ||.-sum(S) + sum(S) - SY.|| by RLVECT_1:5
      .= ||.-sum(S) + SS.|| by RLVECT_1:def 3;
    then ||.SY.|| <= ||.-sum(S).|| + ||.SS.|| by BHSP_1:30;
    then
A13: ||.SY.|| <= ||.sum(S).|| + ||.SS.|| by BHSP_1:31;
    Y02 c= Y1 by A10,XBOOLE_1:11;
    then ||.SS.|| + ||.SY.|| < 1 + (||.sum(S).|| + ||.SS.||) by A3,A11,A13,
XREAL_1:8;
    then ||.SY.|| + ||.SS.|| - ||.SS.|| < 1 + ||.sum(S).|| + ||.SS.|| - ||.SS
    .|| by XREAL_1:14;
    then
A14: ||.sum(S).|| + ||.SY.|| < 1 + ||.sum(S).|| + ||.sum(S).|| by XREAL_1:8;
    0 <= ||.SS.|| by BHSP_1:28;
    then ||.SS.||*(||.sum(S).|| + ||.SY.||) <= ||.SS.||*(2*||.sum(S).|| + 1)
    by A14,XREAL_1:64;
    then ||.SS.||*(||.sum(S).|| + ||.SY.||) + ||.SS.||*(2*||.sum(S).|| + 1) <
    e9*(2*||.sum(S).|| + 1) + ||.SS.||*(2*||.sum(S).|| + 1) by A12,XREAL_1:8;
    then ||.SS.||*(||.sum(S).|| + ||.SY.||) + ||.SS.||*(2*||.sum(S).|| + 1) -
||.SS.||*(2*||.sum(S).|| + 1) < e9*(2*||.sum(S).|| + 1) + ||.SS.||*(2*||.sum(S)
    .|| + 1) - ||.SS.||*(2*||.sum(S).|| + 1) by XREAL_1:14;
    then
A15: ||.SS.||*(||.sum(S).|| + ||.SY.||) < e by A5,XCMPLX_1:87;
    set F = (sum(S)).|.(sum(S)), G = (setsum(Y1)).|.(setsum(Y1));
    abs(F - G) = abs(F - ((sum(S)).|.SY) + (((sum(S)).|.SY) - G))
      .= abs(((sum(S)).|.SS) + (((sum(S)).|.SY) - G)) by BHSP_1:12
      .= abs(((sum(S)).|.SS) + (SS.|.SY)) by BHSP_1:11;
    then
A16: abs(F - G) <= abs(((sum(S)).|.SS)) + abs(SS.|.SY) by COMPLEX1:56;
    abs(((sum(S)).|.SS)) <= ||.sum(S).||*||.SS.|| by BHSP_1:29;
    then
    abs(F - G) + abs(((sum(S)).|.SS)) <= abs(((sum(S)).|.SS)) + abs(SS.|.
    SY) + ||.sum(S).||*||.SS.|| by A16,XREAL_1:7;
    then
    abs(F - G) + abs(((sum(S)).|.SS)) <= (abs(SS.|.SY) + ||.sum(S).||*||.
    SS.||) + abs(((sum(S)).|.SS));
    then
A17: abs(F - G) <= abs(SS.|.SY) + ||.sum(S).||*||.SS.|| by XREAL_1:6;
    abs(SS.|.SY) <= ||.SS.||*||.SY.|| by BHSP_1:29;
    then abs(F - G) + abs(SS.|.SY) <= abs(SS.|.SY) + ||.sum(S).||*||.SS.|| +
    ||.SS.||*||.SY.|| by A17,XREAL_1:7;
    then abs(F - G) + abs(SS.|.SY) <= ||.sum(S).||*||.SS.|| + ||.SS.||*||.SY
    .|| + abs(SS.|.SY);
    then abs(F - G) <= ||.SS.||*||.sum(S).|| + ||.SS.||*||.SY.|| by XREAL_1:6;
    then abs(F - G) + ||.SS.||*(||.sum(S).|| + ||.SY.||) < e + ||.SS.||*(||.
    sum(S).|| + ||.SY.||) by A15,XREAL_1:8;
    then
    abs(F - G) + ||.SS.||*(||.sum(S).|| + ||.SY.||) - ||.SS.||*(||.sum(S)
.|| + ||.SY.||) < e + ||.SS.||*(||.sum(S).|| + ||.SY.||) - ||.SS.||*(||.sum(S)
    .|| + ||.SY.||) by XREAL_1:14;
    hence thesis;
  end;
  Y0 c= S by A7,A2,XBOOLE_1:8;
  hence thesis by A6,A9;
end;

Lm4: for p1, p2 being real number st for e be Real st 0 < e holds abs(p1 - p2)
< e holds p1 = p2
proof
  let p1, p2 be real number;
  assume
A1: for e be Real st 0 < e holds abs(p1 - p2) < e;
  assume p1 <> p2;
  then p1 - p2 <> 0;
  then 0 < abs(p1-p2) by COMPLEX1:47;
  hence contradiction by A1;
end;

theorem
  for X being RealHilbertSpace
   st the addF of X is commutative associative & the addF of X is
  having_a_unity for S be OrthonormalFamily of X for H be
  Functional of X st S c= dom H &
   (for x being Point of X st x in S holds H.x = (x.|.x)) holds S
  is summable_set implies (sum(S)).|.(sum(S)) = sum_byfunc(S, H)
proof
  let X be RealHilbertSpace such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
  let S be OrthonormalFamily of X;
  let H be Functional of X such that
A2: S c= dom H and
A3: for x being Point of X st x in S holds H.x= (x.|.x);
A4: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S holds (setsum(
  Y1)).|.(setsum(Y1)) = setopfunc(Y1, the carrier of X, REAL, H,addreal)
  proof
    let Y1 be finite Subset of X such that
A5: Y1 is non empty and
A6: Y1 c= S;
    Y1 is finite OrthonormalFamily of X by A6,Th5;
    then
A7: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
    for x being Point of X st x in Y1 holds H.x = (x.|.x) by A3,A6;
    hence thesis by A1,A2,A5,A6,A7,Th3,XBOOLE_1:1;
  end;
  set p1 = (sum(S)).|.(sum(S)), p2 = sum_byfunc(S, H);
  assume
A8: S is summable_set;
  then
A9: S is_summable_set_by H by A1,A2,A3,Th6;
  for e be Real st 0 < e holds abs(p1 - p2) < e
  proof
    let e be Real;
    assume 0 < e;
    then
A10: 0/2 < e/2 by XREAL_1:74;
    then consider Y02 be finite Subset of X such that
    Y02 is non empty and
A11: Y02 c= S and
A12: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= S holds abs(p2
- setopfunc(Y1, the carrier of X, REAL, H, addreal)) < e/2 by A9,BHSP_6:def 7;
    consider Y01 be finite Subset of X such that
A13: Y01 is non empty and
A14: Y01 c= S and
A15: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= S holds abs(p1
    - ((setsum Y1).|.(setsum Y1))) < e/2 by A8,A10,Th7;
    set Y1 = Y01 \/ Y02;
A16: Y1 c= S by A14,A11,XBOOLE_1:8;
    reconsider Y011 = Y01 as non empty set by A13;
    set r = setopfunc(Y1, the carrier of X, REAL, H, addreal);
    Y1 = Y011 \/ Y02;
    then (setsum(Y1)).|.(setsum(Y1)) = r by A4,A14,A11,XBOOLE_1:8;
    then Y02 c= Y1 & abs(p1 - r) < e/2 by A15,A16,XBOOLE_1:7;
    then abs(p1-r) + abs(p2-r) < e/2 + e/2 by A12,A16,XREAL_1:8;
    then
A17: abs(p1-r) + abs(r-p2) < e by UNIFORM1:11;
    p1 - p2 = (p1 - r) + (r - p2);
    then abs(p1-p2) <= abs(p1-r) + abs(r-p2) by COMPLEX1:56;
    hence thesis by A17,XXREAL_0:2;
  end;
  hence thesis by Lm4;
end;