bhsp_7.miz



    begin

    reserve X for RealUnitarySpace;

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

    

     Lm1: for x,y,z,e be Real holds |.(x - y).| < (e / 2) & |.(y - z).| < (e / 2) implies |.(x - z).| < e

    proof

      let x,y,z,e be Real;

      assume |.(x - y).| < (e / 2) & |.(y - z).| < (e / 2);

      then |.((x - y) + (y - z)).| <= ( |.(x - y).| + |.(y - z).|) & ( |.(x - y).| + |.(y - z).|) < ((e / 2) + (e / 2)) by COMPLEX1: 56, XREAL_1: 8;

      hence thesis by XXREAL_0: 2;

    end;

    

     Lm2: for p be Real st p > 0 holds ex k be Nat st (1 / (k + 1)) < p

    proof

      let p be Real;

      consider k1 be Nat such that

       A1: (p " ) < k1 by SEQ_4: 3;

      assume p > 0 ;

      then

       A2: 0 < (p " );

      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 be Real, m be Nat st p > 0 holds ex i be Nat st (1 / (i + 1)) < p & i >= m

    proof

      let p be Real, m be Nat;

      consider k1 be Nat such that

       A1: (p " ) < k1 by SEQ_4: 3;

      assume p > 0 ;

      then

       A2: 0 < (p " );

      reconsider i = (k1 + m) as Nat;

      take i;

      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 :: BHSP_7:1

    

     Th1: for Y be Subset of X holds 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 |.( 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 |.( 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 holds 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 |.(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 |.( 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 |.(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 |.( 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 |.(r - ( setopfunc (Y19,the carrier of X, REAL ,L, addreal ))).| < (e / 2) by A3, A4, A5, XBOOLE_1: 8;

            then

             A8: |.(( setopfunc (Y19,the carrier of X, REAL ,L, addreal )) - r).| < (e / 2) by UNIFORM1: 11;

             |.(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 |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < e;

      ex r be Real st 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 Y0 c= Y1 & Y1 c= Y holds |.(r - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e

      proof

        defpred P[ object, object] means ex D2 be set st D2 = $2 & $2 is finite Subset of X & D2 is non empty & D2 c= Y & for z be Real st z = $1 holds for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & D2 misses Y1 holds |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < (1 / (z + 1));

        

         A10: for x be object st x in NAT holds ex y be object st y in ( bool Y) & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider xx = x as Element of NAT ;

          reconsider e = (1 / (xx + 1)) as Real;

          ( 0 / (xx + 1)) < (1 / (xx + 1)) by XREAL_1: 74;

          then

          consider Y0 be finite Subset of X such that

           A11: Y0 is non empty and

           A12: Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < e by A9;

          take Y0;

          thus Y0 in ( bool Y) by A12, ZFMISC_1:def 1;

          take D2 = Y0;

          thus D2 = Y0;

          thus Y0 is finite Subset of X;

          thus D2 is non empty by A11;

          thus D2 c= Y by A12;

          for z be Real st z = x holds for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < (1 / (z + 1)) by A12;

          hence for z be Real st z = x holds for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & D2 misses Y1 holds |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < (1 / (z + 1));

        end;

        

         A13: ex B be sequence of ( bool Y) st for x be object st x in NAT holds P[x, (B . x)] from FUNCT_2:sch 1( A10);

        ex A be sequence of ( bool Y) st for i be 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 |.( 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 be sequence of ( bool Y) such that

           A14: for x be object st x in NAT holds P[x, (B . x)] by A13;

          

           A15: for x be object 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 holds for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & (B . x) misses Y1 holds |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < (1 / (z + 1))

          proof

            let x be object such that

             A16: x in NAT ;

             P[x, (B . x)] by A16, A14;

            hence (B . x) is finite Subset of X & (B . x) is non empty & (B . x) c= Y & for z be Real st z = x holds for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & (B . x) misses Y1 holds |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < (1 / (z + 1));

          end;

          deffunc G( Nat, set) = ((B . ($1 + 1)) \/ $2);

          ex A be Function st ( dom A) = NAT & (A . 0 ) = (B . 0 ) & for n be Nat holds (A . (n + 1)) = G(n,.) from NAT_1:sch 11;

          then

          consider A be Function such that

           A17: ( dom A) = NAT and

           A18: (A . 0 ) = (B . 0 ) and

           A19: for n be Nat holds (A . (n + 1)) = ((B . (n + 1)) \/ (A . n));

          defpred R[ 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 |.( 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);

           A20:

          now

            let n be Nat such that

             A21: R[n];

            

             A22: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & (A . (n + 1)) misses Y1 holds |.( setopfunc (Y1,the carrier of X, REAL ,L, addreal )).| < (1 / ((n + 1) + 1))

            proof

              let Y1 be finite Subset of X such that

               A23: Y1 is non empty & Y1 c= Y and

               A24: (A . (n + 1)) misses Y1;

              (A . (n + 1)) = ((B . (n + 1)) \/ (A . n)) by A19;

              then (B . (n + 1)) misses Y1 by A24, XBOOLE_1: 7, XBOOLE_1: 63;

              hence thesis by A15, A23;

            end;

            defpred P[ Nat] means (n + 1) <= $1 implies (A . (n + 1)) c= (A . $1);

            

             A25: for j be Nat st P[j] holds P[(j + 1)]

            proof

              let j be Nat such that

               A26: P[j] and

               A27: (n + 1) <= (j + 1);

              now

                per cases ;

                  case n = j;

                  hence thesis;

                end;

                  case

                   A28: n <> j;

                  (A . (j + 1)) = ((B . (j + 1)) \/ (A . j)) by A19;

                  then

                   A29: (A . j) c= (A . (j + 1)) by XBOOLE_1: 7;

                  n <= j by A27, XREAL_1: 6;

                  then n < j by A28, XXREAL_0: 1;

                  hence thesis by A26, A29, NAT_1: 13;

                end;

              end;

              hence thesis;

            end;

            

             A30: P[ 0 ];

            

             A31: for j be Nat holds P[j] from NAT_1:sch 2( A30, A25);

            (A . (n + 1)) = ((B . (n + 1)) \/ (A . n)) & (B . (n + 1)) is finite Subset of X by A15, A19;

            hence R[(n + 1)] by A21, A22, A31, XBOOLE_1: 8;

          end;

          for j0 be Nat st j0 = 0 holds for j be Nat st j0 <= j holds (A . j0) c= (A . j)

          proof

            let j0 be Nat such that

             A32: j0 = 0 ;

            defpred P[ Nat] means j0 <= $1 implies (A . j0) c= (A . $1);

             A33:

            now

              let j be Nat such that

               A34: P[j];

              (A . (j + 1)) = ((B . (j + 1)) \/ (A . j)) by A19;

              then (A . j) c= (A . (j + 1)) by XBOOLE_1: 7;

              hence P[(j + 1)] by A32, A34, XBOOLE_1: 1;

            end;

            

             A35: P[ 0 ] by A32;

            thus for j be Nat holds P[j] from NAT_1:sch 2( A35, A33);

          end;

          then

           A36: R[ 0 ] by A15, A18;

          

           A37: for i be Nat holds R[i] from NAT_1:sch 2( A36, A20);

          ( rng A) c= ( bool Y)

          proof

            let y be object;

            assume y in ( rng A);

            then

            consider x be object such that

             A38: x in ( dom A) and

             A39: y = (A . x) by FUNCT_1:def 3;

            reconsider i = x as Element of NAT by A17, A38;

            (A . i) c= Y by A37;

            hence thesis by A39, ZFMISC_1:def 1;

          end;

          then A is sequence of ( bool Y) by A17, FUNCT_2: 2;

          hence thesis by A37;

        end;

        then

        consider A be sequence of ( bool Y) such that

         A40: for i be 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 |.( 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[ object, object] 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 ));

        

         A41: for x be object st x in NAT holds ex y be object st y in REAL & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Element of NAT ;

          (A . i) is finite Subset of X by A40;

          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 A40;

          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 be sequence of REAL st for x be object st x in NAT holds P[x, (F . x)] from FUNCT_2:sch 1( A41);

        then

        consider F be sequence of REAL such that

         A42: for x be object 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;

        

         A43: for e be Real st e > 0 holds ex k be Nat st for n,m be Nat st n >= k & m >= k holds |.((seq . n) - (seq . m) qua Real).| < e

        proof

          let e be Real such that

           A44: e > 0 ;

          

           A45: (e / 2) > ( 0 / 2) by A44, XREAL_1: 74;

          then

          consider k be Nat such that

           A46: (1 / (k + 1)) < (e / 2) by Lm2;

          take k;

          let nn,mm be Nat such that

           A47: nn >= k and

           A48: mm >= k;

          reconsider m = mm, n = nn, k as Element of NAT by ORDINAL1:def 12;

          consider Y2 be finite Subset of X such that Y2 is non empty and

           A49: (A . m) = Y2 and

           A50: (seq . m) = ( setopfunc (Y2,the carrier of X, REAL ,L, addreal )) by A42;

          consider Y0 be finite Subset of X such that Y0 is non empty and

           A51: (A . k) = Y0 and (seq . k) = ( setopfunc (Y0,the carrier of X, REAL ,L, addreal )) by A42;

          

           A52: Y0 c= Y2 by A40, A48, A51, A49;

          consider Y1 be finite Subset of X such that Y1 is non empty and

           A53: (A . n) = Y1 and

           A54: (seq . n) = ( setopfunc (Y1,the carrier of X, REAL ,L, addreal )) by A42;

          

           A55: Y0 c= Y1 by A40, A47, A51, A53;

          now

            per cases ;

              case

               A56: Y0 = Y1;

              now

                per cases ;

                  case Y0 = Y2;

                  hence thesis by A44, A54, A50, A56, ABSVALUE: 2;

                end;

                  case

                   A57: 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);

                    

                     A58: (Y2 \ Y0) c= Y2 by XBOOLE_1: 36;

                    (Y0 \/ Y02) = (Y0 \/ Y2) by XBOOLE_1: 39

                    .= Y2 by A52, XBOOLE_1: 12;

                    hence thesis by A49, A57, A58, XBOOLE_1: 1, XBOOLE_1: 79;

                  end;

                  then

                  consider Y02 be finite Subset of X such that

                   A59: Y02 is non empty & Y02 c= Y and

                   A60: Y02 misses Y0 and

                   A61: (Y0 \/ Y02) = Y2;

                   |.( setopfunc (Y02,the carrier of X, REAL ,L, addreal )).| < (1 / (k + 1)) by A40, A51, A59, A60;

                  then

                   A62: |.( setopfunc (Y02,the carrier of X, REAL ,L, addreal )).| < (e / 2) by A46, 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 A60, A61, 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

                   A63: |.((seq . n) - (seq . m)).| = |.( - ( setopfunc (Y02,the carrier of X, REAL ,L, addreal ))).| by A54, A50, A56

                  .= |.( setopfunc (Y02,the carrier of X, REAL ,L, addreal )).| by COMPLEX1: 52;

                  (e / 2) < e by A44, XREAL_1: 216;

                  hence thesis by A62, A63, XXREAL_0: 2;

                end;

              end;

              hence thesis;

            end;

              case

               A64: Y0 <> Y1;

              now

                per cases ;

                  case

                   A65: 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);

                    

                     A66: (Y1 \ Y0) c= Y1 by XBOOLE_1: 36;

                    (Y0 \/ Y01) = (Y0 \/ Y1) by XBOOLE_1: 39

                    .= Y1 by A55, XBOOLE_1: 12;

                    hence thesis by A53, A64, A66, XBOOLE_1: 1, XBOOLE_1: 79;

                  end;

                  then

                  consider Y01 be finite Subset of X such that

                   A67: Y01 is non empty & Y01 c= Y and

                   A68: Y01 misses Y0 and

                   A69: (Y0 \/ Y01) = Y1;

                  ( dom L) = the carrier of X by FUNCT_2:def 1;

                  

                  then

                   A70: ( 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 A68, A69, 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;

                   |.( setopfunc (Y01,the carrier of X, REAL ,L, addreal )).| < (1 / (k + 1)) by A40, A51, A67, A68;

                  then |.((seq . n) - (seq . m)).| < (e / 2) by A46, A54, A50, A65, A70, XXREAL_0: 2;

                  then ( |.((seq . n) - (seq . m)).| + 0 ) < ((e / 2) + (e / 2)) by A45, XREAL_1: 8;

                  hence thesis;

                end;

                  case

                   A71: 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);

                    

                     A72: (Y2 \ Y0) c= Y2 by XBOOLE_1: 36;

                    (Y0 \/ Y02) = (Y0 \/ Y2) by XBOOLE_1: 39

                    .= Y2 by A52, XBOOLE_1: 12;

                    hence thesis by A49, A71, A72, XBOOLE_1: 1, XBOOLE_1: 79;

                  end;

                  then

                  consider Y02 be finite Subset of X such that

                   A73: Y02 is non empty & Y02 c= Y and

                   A74: Y02 misses Y0 and

                   A75: (Y0 \/ Y02) = Y2;

                  ( dom L) = the carrier of X by FUNCT_2:def 1;

                  

                  then

                   A76: ( 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 A74, A75, 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);

                    

                     A77: (Y1 \ Y0) c= Y1 by XBOOLE_1: 36;

                    (Y0 \/ Y01) = (Y0 \/ Y1) by XBOOLE_1: 39

                    .= Y1 by A55, XBOOLE_1: 12;

                    hence thesis by A53, A64, A77, XBOOLE_1: 1, XBOOLE_1: 79;

                  end;

                  then

                  consider Y01 be finite Subset of X such that

                   A78: Y01 is non empty & Y01 c= Y and

                   A79: Y01 misses Y0 and

                   A80: (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 A79, A80, 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 A54, A50, A76;

                  then

                   A81: |.((seq . n) - (seq . m)).| <= ( |.( setopfunc (Y01,the carrier of X, REAL ,L, addreal )).| + |.( setopfunc (Y02,the carrier of X, REAL ,L, addreal )).|) by COMPLEX1: 57;

                   |.( setopfunc (Y02,the carrier of X, REAL ,L, addreal )).| < (1 / (k + 1)) by A40, A51, A73, A74;

                  then

                   A82: |.( setopfunc (Y02,the carrier of X, REAL ,L, addreal )).| < (e / 2) by A46, XXREAL_0: 2;

                   |.( setopfunc (Y01,the carrier of X, REAL ,L, addreal )).| < (1 / (k + 1)) by A40, A51, A78, A79;

                  then |.( setopfunc (Y01,the carrier of X, REAL ,L, addreal )).| < (e / 2) by A46, XXREAL_0: 2;

                  then ( |.( setopfunc (Y01,the carrier of X, REAL ,L, addreal )).| + |.( setopfunc (Y02,the carrier of X, REAL ,L, addreal )).|) < ((e / 2) + (e / 2)) by A82, XREAL_1: 8;

                  hence thesis by A81, XXREAL_0: 2;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        for e be Real st 0 < e holds ex k be Nat st for m be Nat st k <= m holds |.((seq . m) - (seq . k)).| < e

        proof

          let e be Real;

          assume 0 < e;

          then

          consider k be Nat such that

           A83: for n,m be Nat st n >= k & m >= k holds |.((seq . n) - (seq . m)).| < e by A43;

          for m be Nat st k <= m holds |.((seq . m) - (seq . k)).| < e by A83;

          hence thesis;

        end;

        then seq is convergent by SEQ_4: 41;

        then

        consider x be Real such that

         A84: for r be Real st r > 0 holds ex m be Nat st for n be Nat st n >= m holds |.((seq . n) - x).| < r by SEQ_2:def 6;

        reconsider r = x as Real;

        take r;

        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 Y0 c= Y1 & Y1 c= Y holds |.(r - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e

        proof

          let e be Real;

          assume e > 0 ;

          then

           A85: (e / 2) > ( 0 / 2) by XREAL_1: 74;

          then

          consider m be Nat such that

           A86: for n be Nat st n >= m holds |.((seq . n) - r).| < (e / 2) by A84;

          consider i be Nat such that

           A87: (1 / (i + 1)) < (e / 2) and

           A88: i >= m by A85, Lm3;

          i in NAT by ORDINAL1:def 12;

          then

          reconsider ii = i as Element of NAT ;

          consider Y0 be finite Subset of X such that

           A89: Y0 is non empty and

           A90: (A . ii) = Y0 and

           A91: (seq . i) = ( setopfunc (Y0,the carrier of X, REAL ,L, addreal )) by A42;

          

           A92: |.(( setopfunc (Y0,the carrier of X, REAL ,L, addreal )) - r).| < (e / 2) by A86, A88, A91;

          now

            let Y1 be finite Subset of X such that

             A93: Y0 c= Y1 and

             A94: Y1 c= Y;

            now

              per cases ;

                case Y0 = Y1;

                then |.(r - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < (e / 2) by A92, UNIFORM1: 11;

                then ( |.(x - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| + 0 ) < ((e / 2) + (e / 2)) by A85, XREAL_1: 8;

                hence |.(r - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e;

              end;

                case

                 A95: 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);

                  

                   A96: (Y1 \ Y0) c= Y1 by XBOOLE_1: 36;

                  (Y0 \/ Y2) = (Y0 \/ Y1) by XBOOLE_1: 39

                  .= Y1 by A93, XBOOLE_1: 12;

                  hence thesis by A94, A95, A96, XBOOLE_1: 79;

                end;

                then

                consider Y2 be finite Subset of X such that

                 A97: Y2 is non empty & Y2 c= Y and

                 A98: Y0 misses Y2 and

                 A99: (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 A98, A99, 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 |.(( setopfunc (Y1,the carrier of X, REAL ,L, addreal )) - r).| <= ( |.(( setopfunc (Y0,the carrier of X, REAL ,L, addreal )) - r).| + |.( setopfunc (Y2,the carrier of X, REAL ,L, addreal )).|) by ABSVALUE: 9;

                then

                 A100: |.(x - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| <= ( |.(( setopfunc (Y0,the carrier of X, REAL ,L, addreal )) - r).| + |.( setopfunc (Y2,the carrier of X, REAL ,L, addreal )).|) by UNIFORM1: 11;

                 |.( setopfunc (Y2,the carrier of X, REAL ,L, addreal )).| < (1 / (i + 1)) by A40, A90, A97, A98;

                then |.( setopfunc (Y2,the carrier of X, REAL ,L, addreal )).| < (e / 2) by A87, XXREAL_0: 2;

                then ( |.(( setopfunc (Y0,the carrier of X, REAL ,L, addreal )) - r).| + |.( setopfunc (Y2,the carrier of X, REAL ,L, addreal )).|) < ((e / 2) + (e / 2)) by A92, XREAL_1: 8;

                hence |.(r - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e by A100, XXREAL_0: 2;

              end;

            end;

            hence |.(r - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e;

          end;

          hence thesis by A89, A90;

        end;

        hence thesis;

      end;

      hence thesis by BHSP_6:def 6;

    end;

    theorem :: BHSP_7:2

    

     Th2: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for S be finite OrthogonalFamily of X st S is non empty holds 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) holds 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, 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 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 :: BHSP_7:3

    

     Th3: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for S be finite OrthogonalFamily of X st S is non empty holds 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;

      

       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 :: BHSP_7:4

    

     Th4: for Y be OrthogonalFamily of X holds 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 :: BHSP_7:5

    

     Th5: for Y be OrthonormalFamily of X holds 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

    theorem :: BHSP_7:6

    

     Th6: for X be RealHilbertSpace st the addF of X is commutative associative & the addF of X is having_a_unity holds for S be OrthonormalFamily of X holds for H be Functional of X st S c= ( dom H) & (for x be 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 be 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 Element of 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 be 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, BHSP_1: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 |.( 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 |.( 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;

             |.F.| < e1 by A22, A23, A24, A25;

            then (F - e1) < ( |.F.| - |.F.|) by ABSVALUE: 4, XREAL_1: 15;

            then

             A27: F < e1 by XREAL_1: 48;

            for x be 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, BHSP_1: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 :: BHSP_7:7

    

     Th7: for S be Subset of X st S is summable_set holds for e be Real st 0 < e holds 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 |.((( 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).||);

      then

       A5: ( 0 + 0 ) < ((2 * ||.( sum S).||) + 1);

      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 |.((( 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));

         |.(F - G).| = |.((F - (( sum S) .|. SY)) + ((( sum S) .|. SY) - G)).|

        .= |.((( sum S) .|. SS) + ((( sum S) .|. SY) - G)).| by BHSP_1: 12

        .= |.((( sum S) .|. SS) + (SS .|. SY)).| by BHSP_1: 11;

        then

         A16: |.(F - G).| <= ( |.(( sum S) .|. SS).| + |.(SS .|. SY).|) by COMPLEX1: 56;

         |.(( sum S) .|. SS).| <= ( ||.( sum S).|| * ||.SS.||) by BHSP_1: 29;

        then ( |.(F - G).| + |.(( sum S) .|. SS).|) <= (( |.(( sum S) .|. SS).| + |.(SS .|. SY).|) + ( ||.( sum S).|| * ||.SS.||)) by A16, XREAL_1: 7;

        then ( |.(F - G).| + |.(( sum S) .|. SS).|) <= (( |.(SS .|. SY).| + ( ||.( sum S).|| * ||.SS.||)) + |.(( sum S) .|. SS).|);

        then

         A17: |.(F - G).| <= ( |.(SS .|. SY).| + ( ||.( sum S).|| * ||.SS.||)) by XREAL_1: 6;

         |.(SS .|. SY).| <= ( ||.SS.|| * ||.SY.||) by BHSP_1: 29;

        then ( |.(F - G).| + |.(SS .|. SY).|) <= (( |.(SS .|. SY).| + ( ||.( sum S).|| * ||.SS.||)) + ( ||.SS.|| * ||.SY.||)) by A17, XREAL_1: 7;

        then ( |.(F - G).| + |.(SS .|. SY).|) <= ((( ||.( sum S).|| * ||.SS.||) + ( ||.SS.|| * ||.SY.||)) + |.(SS .|. SY).|);

        then |.(F - G).| <= (( ||.SS.|| * ||.( sum S).||) + ( ||.SS.|| * ||.SY.||)) by XREAL_1: 6;

        then ( |.(F - G).| + ( ||.SS.|| * ( ||.( sum S).|| + ||.SY.||))) < (e + ( ||.SS.|| * ( ||.( sum S).|| + ||.SY.||))) by A15, XREAL_1: 8;

        then (( |.(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 be Real st for e be Real st 0 < e holds |.(p1 - p2).| < e holds p1 = p2

    proof

      let p1,p2 be Real;

      assume

       A1: for e be Real st 0 < e holds |.(p1 - p2).| < e;

      assume p1 <> p2;

      then (p1 - p2) <> 0 ;

      then 0 < |.(p1 - p2).| by COMPLEX1: 47;

      hence contradiction by A1;

    end;

    theorem :: BHSP_7:8

    for X be RealHilbertSpace st the addF of X is commutative associative & the addF of X is having_a_unity holds for S be OrthonormalFamily of X holds for H be Functional of X st S c= ( dom H) & (for x be 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 be 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 be 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 |.(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 |.(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 |.(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 & |.(p1 - r).| < (e / 2) by A15, A16, XBOOLE_1: 7;

        then ( |.(p1 - r).| + |.(p2 - r).|) < ((e / 2) + (e / 2)) by A12, A16, XREAL_1: 8;

        then

         A17: ( |.(p1 - r).| + |.(r - p2).|) < e by UNIFORM1: 11;

        (p1 - p2) = ((p1 - r) + (r - p2));

        then |.(p1 - p2).| <= ( |.(p1 - r).| + |.(r - p2).|) by COMPLEX1: 56;

        hence thesis by A17, XXREAL_0: 2;

      end;

      hence thesis by Lm4;

    end;