bhsp_4.miz

    begin

    reserve a,b,r,M2 for Real;

    reserve Rseq,Rseq1,Rseq2 for Real_Sequence;

    reserve k,n,m,m1,m2 for Nat;

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

    definition

      let X be non empty addLoopStr;

      let seq be sequence of X;

      :: BHSP_4:def1

      func Partial_Sums (seq) -> sequence of X means

      : Def1: (it . 0 ) = (seq . 0 ) & for n holds (it . (n + 1)) = ((it . n) + (seq . (n + 1)));

      existence

      proof

        deffunc G( Nat, Point of X) = ($2 + (seq . ($1 + 1)));

        consider f be sequence of the carrier of X such that

         A1: (f . 0 ) = (seq . 0 ) & for n be Nat holds (f . (n + 1)) = G(n,.) from NAT_1:sch 12;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let seq1,seq2 be sequence of X;

        assume that

         A2: (seq1 . 0 ) = (seq . 0 ) and

         A3: for n holds (seq1 . (n + 1)) = ((seq1 . n) + (seq . (n + 1))) and

         A4: (seq2 . 0 ) = (seq . 0 ) and

         A5: for n holds (seq2 . (n + 1)) = ((seq2 . n) + (seq . (n + 1)));

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);



         A6: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume (seq1 . k) = (seq2 . k);



          hence (seq1 . (k + 1)) = ((seq2 . k) + (seq . (k + 1))) by A3

          .= (seq2 . (k + 1)) by A5;

        end;



         A7: P[ 0 ] by A2, A4;

        for n holds P[n] from NAT_1:sch 2( A7, A6);

        then for n be Element of NAT holds P[n];

        hence seq1 = seq2;

      end;

    end

    theorem :: BHSP_4:1



     Th1: for X be Abelian add-associative non empty addLoopStr, seq1,seq2 be sequence of X holds (( Partial_Sums seq1) + ( Partial_Sums seq2)) = ( Partial_Sums (seq1 + seq2))

    proof

      let X be Abelian add-associative non empty addLoopStr, seq1,seq2 be sequence of X;

      set PSseq1 = ( Partial_Sums seq1);

      set PSseq2 = ( Partial_Sums seq2);

       A1:

      now

        let n;



        thus ((PSseq1 + PSseq2) . (n + 1)) = ((PSseq1 . (n + 1)) + (PSseq2 . (n + 1))) by NORMSP_1:def 2

        .= (((PSseq1 . n) + (seq1 . (n + 1))) + (PSseq2 . (n + 1))) by Def1

        .= (((PSseq1 . n) + (seq1 . (n + 1))) + ((seq2 . (n + 1)) + (PSseq2 . n))) by Def1

        .= ((((PSseq1 . n) + (seq1 . (n + 1))) + (seq2 . (n + 1))) + (PSseq2 . n)) by RLVECT_1:def 3

        .= (((PSseq1 . n) + ((seq1 . (n + 1)) + (seq2 . (n + 1)))) + (PSseq2 . n)) by RLVECT_1:def 3

        .= (((PSseq1 . n) + ((seq1 + seq2) . (n + 1))) + (PSseq2 . n)) by NORMSP_1:def 2

        .= (((PSseq1 . n) + (PSseq2 . n)) + ((seq1 + seq2) . (n + 1))) by RLVECT_1:def 3

        .= (((PSseq1 + PSseq2) . n) + ((seq1 + seq2) . (n + 1))) by NORMSP_1:def 2;

      end;

      ((PSseq1 + PSseq2) . 0 ) = ((PSseq1 . 0 ) + (PSseq2 . 0 )) by NORMSP_1:def 2

      .= ((seq1 . 0 ) + (PSseq2 . 0 )) by Def1

      .= ((seq1 . 0 ) + (seq2 . 0 )) by Def1

      .= ((seq1 + seq2) . 0 ) by NORMSP_1:def 2;

      hence thesis by A1, Def1;

    end;

    theorem :: BHSP_4:2



     Th2: for X be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, seq1,seq2 be sequence of X holds (( Partial_Sums seq1) - ( Partial_Sums seq2)) = ( Partial_Sums (seq1 - seq2))

    proof

      let X be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, seq1,seq2 be sequence of X;

      set PSseq1 = ( Partial_Sums seq1);

      set PSseq2 = ( Partial_Sums seq2);

       A1:

      now

        let n;



        thus ((PSseq1 - PSseq2) . (n + 1)) = ((PSseq1 . (n + 1)) - (PSseq2 . (n + 1))) by NORMSP_1:def 3

        .= (((PSseq1 . n) + (seq1 . (n + 1))) - (PSseq2 . (n + 1))) by Def1

        .= (((PSseq1 . n) + (seq1 . (n + 1))) - ((seq2 . (n + 1)) + (PSseq2 . n))) by Def1

        .= ((((PSseq1 . n) + (seq1 . (n + 1))) - (seq2 . (n + 1))) - (PSseq2 . n)) by RLVECT_1: 27

        .= (((PSseq1 . n) + ((seq1 . (n + 1)) - (seq2 . (n + 1)))) - (PSseq2 . n)) by RLVECT_1:def 3

        .= (((PSseq1 . n) - (PSseq2 . n)) + ((seq1 . (n + 1)) - (seq2 . (n + 1)))) by RLVECT_1:def 3

        .= (((PSseq1 - PSseq2) . n) + ((seq1 . (n + 1)) - (seq2 . (n + 1)))) by NORMSP_1:def 3

        .= (((PSseq1 - PSseq2) . n) + ((seq1 - seq2) . (n + 1))) by NORMSP_1:def 3;

      end;

      ((PSseq1 - PSseq2) . 0 ) = ((PSseq1 . 0 ) - (PSseq2 . 0 )) by NORMSP_1:def 3

      .= ((seq1 . 0 ) - (PSseq2 . 0 )) by Def1

      .= ((seq1 . 0 ) - (seq2 . 0 )) by Def1

      .= ((seq1 - seq2) . 0 ) by NORMSP_1:def 3;

      hence thesis by A1, Def1;

    end;

    theorem :: BHSP_4:3



     Th3: for X be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, seq be sequence of X holds ( Partial_Sums (a * seq)) = (a * ( Partial_Sums seq))

    proof

      let X be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, seq be sequence of X;

      set PSseq = ( Partial_Sums seq);

       A1:

      now

        let n;



        thus ((a * PSseq) . (n + 1)) = (a * (PSseq . (n + 1))) by NORMSP_1:def 5

        .= (a * ((PSseq . n) + (seq . (n + 1)))) by Def1

        .= ((a * (PSseq . n)) + (a * (seq . (n + 1)))) by RLVECT_1:def 5

        .= (((a * PSseq) . n) + (a * (seq . (n + 1)))) by NORMSP_1:def 5

        .= (((a * PSseq) . n) + ((a * seq) . (n + 1))) by NORMSP_1:def 5;

      end;

      ((a * PSseq) . 0 ) = (a * (PSseq . 0 )) by NORMSP_1:def 5

      .= (a * (seq . 0 )) by Def1

      .= ((a * seq) . 0 ) by NORMSP_1:def 5;

      hence thesis by A1, Def1;

    end;

    reserve X for RealUnitarySpace;

    reserve g for Point of X;

    reserve seq,seq1,seq2 for sequence of X;

    theorem :: BHSP_4:4

    ( Partial_Sums ( - seq)) = ( - ( Partial_Sums seq))

    proof

      ( Partial_Sums (( - 1) * seq)) = (( - 1) * ( Partial_Sums seq)) by Th3;

      then ( Partial_Sums ( - seq)) = (( - 1) * ( Partial_Sums seq)) by BHSP_1: 55;

      hence thesis by BHSP_1: 55;

    end;

    theorem :: BHSP_4:5

    ((a * ( Partial_Sums seq1)) + (b * ( Partial_Sums seq2))) = ( Partial_Sums ((a * seq1) + (b * seq2)))

    proof



      thus ((a * ( Partial_Sums seq1)) + (b * ( Partial_Sums seq2))) = (( Partial_Sums (a * seq1)) + (b * ( Partial_Sums seq2))) by Th3

      .= (( Partial_Sums (a * seq1)) + ( Partial_Sums (b * seq2))) by Th3

      .= ( Partial_Sums ((a * seq1) + (b * seq2))) by Th1;

    end;

    definition

      let X, seq;

      :: BHSP_4:def2

      attr seq is summable means

      : Def2: ( Partial_Sums seq) is convergent;

      :: BHSP_4:def3

      func Sum (seq) -> Point of X equals ( lim ( Partial_Sums seq));

      coherence ;

    end

    theorem :: BHSP_4:6

    seq1 is summable & seq2 is summable implies (seq1 + seq2) is summable & ( Sum (seq1 + seq2)) = (( Sum seq1) + ( Sum seq2))

    proof

      assume seq1 is summable & seq2 is summable;

      then

       A1: ( Partial_Sums seq1) is convergent & ( Partial_Sums seq2) is convergent;

      then (( Partial_Sums seq1) + ( Partial_Sums seq2)) is convergent by BHSP_2: 3;

      then ( Partial_Sums (seq1 + seq2)) is convergent by Th1;

      hence (seq1 + seq2) is summable;



      thus ( Sum (seq1 + seq2)) = ( lim (( Partial_Sums seq1) + ( Partial_Sums seq2))) by Th1

      .= (( Sum seq1) + ( Sum seq2)) by A1, BHSP_2: 13;

    end;

    theorem :: BHSP_4:7

    seq1 is summable & seq2 is summable implies (seq1 - seq2) is summable & ( Sum (seq1 - seq2)) = (( Sum seq1) - ( Sum seq2))

    proof

      assume seq1 is summable & seq2 is summable;

      then

       A1: ( Partial_Sums seq1) is convergent & ( Partial_Sums seq2) is convergent;

      then (( Partial_Sums seq1) - ( Partial_Sums seq2)) is convergent by BHSP_2: 4;

      then ( Partial_Sums (seq1 - seq2)) is convergent by Th2;

      hence (seq1 - seq2) is summable;



      thus ( Sum (seq1 - seq2)) = ( lim (( Partial_Sums seq1) - ( Partial_Sums seq2))) by Th2

      .= (( Sum seq1) - ( Sum seq2)) by A1, BHSP_2: 14;

    end;

    theorem :: BHSP_4:8

    seq is summable implies (a * seq) is summable & ( Sum (a * seq)) = (a * ( Sum seq))

    proof

      assume seq is summable;

      then

       A1: ( Partial_Sums seq) is convergent;

      then (a * ( Partial_Sums seq)) is convergent by BHSP_2: 5;

      then ( Partial_Sums (a * seq)) is convergent by Th3;

      hence (a * seq) is summable;



      thus ( Sum (a * seq)) = ( lim (a * ( Partial_Sums seq))) by Th3

      .= (a * ( Sum seq)) by A1, BHSP_2: 15;

    end;

    theorem :: BHSP_4:9



     Th9: seq is summable implies seq is convergent & ( lim seq) = ( 0. X)

    proof

      set PSseq = ( Partial_Sums seq);

      now

        let n;

        (PSseq . (n + 1)) = ((PSseq . n) + (seq . (n + 1))) by Def1

        .= ((PSseq . n) + ((seq ^\ 1) . n)) by NAT_1:def 3;

        hence ((PSseq ^\ 1) . n) = ((PSseq . n) + ((seq ^\ 1) . n)) by NAT_1:def 3;

      end;

      then

       A1: (PSseq ^\ 1) = (PSseq + (seq ^\ 1)) by NORMSP_1:def 2;

      ((seq ^\ 1) + (PSseq - PSseq)) = (seq ^\ 1)

      proof

        let n be Element of NAT ;



        thus (((seq ^\ 1) + (PSseq - PSseq)) . n) = (((seq ^\ 1) . n) + ((PSseq - PSseq) . n)) by NORMSP_1:def 2

        .= (((seq ^\ 1) . n) + ((PSseq . n) - (PSseq . n))) by NORMSP_1:def 3

        .= (((seq ^\ 1) . n) + 09(X)) by RLVECT_1: 15

        .= ((seq ^\ 1) . n);

      end;

      then

       A2: (seq ^\ 1) = ((PSseq ^\ 1) - PSseq) by A1, BHSP_1: 61;

      assume seq is summable;

      then

       A3: PSseq is convergent;



       A4: (seq ^\ 1) is convergent by A3, A2, BHSP_2: 4;

      hence seq is convergent by BHSP_3: 37;

      ( lim (PSseq ^\ 1)) = ( lim PSseq) by A3, BHSP_3: 36;



      then ( lim ((PSseq ^\ 1) - PSseq)) = (( lim PSseq) - ( lim PSseq)) by A3, BHSP_2: 14

      .= 09(X) by RLVECT_1: 15;

      hence thesis by A2, A4, BHSP_3: 28, BHSP_3: 37;

    end;

    theorem :: BHSP_4:10



     Th10: for X be RealHilbertSpace, seq be sequence of X holds seq is summable iff for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.((( Partial_Sums seq) . n) - (( Partial_Sums seq) . m)).|| < r by BHSP_3: 2, BHSP_3:def 4;

    theorem :: BHSP_4:11

    seq is summable implies ( Partial_Sums seq) is bounded;

    theorem :: BHSP_4:12



     Th12: for seq, seq1 st for n holds (seq1 . n) = (seq . 0 ) holds ( Partial_Sums (seq ^\ 1)) = ((( Partial_Sums seq) ^\ 1) - seq1)

    proof

      let seq, seq1;

      assume

       A1: for n holds (seq1 . n) = (seq . 0 );

       A2:

      now

        let n;



        thus (((( Partial_Sums seq) ^\ 1) - seq1) . (n + 1)) = (((( Partial_Sums seq) ^\ 1) . (n + 1)) - (seq1 . (n + 1))) by NORMSP_1:def 3

        .= (((( Partial_Sums seq) ^\ 1) . (n + 1)) - (seq . 0 )) by A1

        .= ((( Partial_Sums seq) . ((n + 1) + 1)) - (seq . 0 )) by NAT_1:def 3

        .= (((seq . ((n + 1) + 1)) + (( Partial_Sums seq) . (n + 1))) - (seq . 0 )) by Def1

        .= (((seq . ((n + 1) + 1)) + (( Partial_Sums seq) . (n + 1))) - (seq1 . n)) by A1

        .= ((seq . ((n + 1) + 1)) + ((( Partial_Sums seq) . (n + 1)) - (seq1 . n))) by RLVECT_1:def 3

        .= ((seq . ((n + 1) + 1)) + (((( Partial_Sums seq) ^\ 1) . n) - (seq1 . n))) by NAT_1:def 3

        .= ((seq . ((n + 1) + 1)) + (((( Partial_Sums seq) ^\ 1) - seq1) . n)) by NORMSP_1:def 3

        .= ((((( Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1))) by NAT_1:def 3;

      end;

      (((( Partial_Sums seq) ^\ 1) - seq1) . 0 ) = (((( Partial_Sums seq) ^\ 1) . 0 ) - (seq1 . 0 )) by NORMSP_1:def 3

      .= (((( Partial_Sums seq) ^\ 1) . 0 ) - (seq . 0 )) by A1

      .= ((( Partial_Sums seq) . ( 0 + 1)) - (seq . 0 )) by NAT_1:def 3

      .= (((( Partial_Sums seq) . 0 ) + (seq . ( 0 + 1))) - (seq . 0 )) by Def1

      .= (((seq . ( 0 + 1)) + (seq . 0 )) - (seq . 0 )) by Def1

      .= ((seq . ( 0 + 1)) + ((seq . 0 ) - (seq . 0 ))) by RLVECT_1:def 3

      .= ((seq . ( 0 + 1)) + 09(X)) by RLVECT_1: 15

      .= (seq . ( 0 + 1))

      .= ((seq ^\ 1) . 0 ) by NAT_1:def 3;

      hence thesis by A2, Def1;

    end;

    theorem :: BHSP_4:13



     Th13: seq is summable implies for k holds (seq ^\ k) is summable

    proof

      defpred P[ Nat] means (seq ^\ $1) is summable;



       A1: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        reconsider seq1 = ( NAT --> ((seq ^\ k) . 0 )) as sequence of X;

        assume (seq ^\ k) is summable;

        then

         A2: ( Partial_Sums (seq ^\ k)) is convergent;

        for m holds (seq1 . m) = ((seq ^\ k) . 0 ) by ORDINAL1:def 12, FUNCOP_1: 7;

        then seq1 is convergent & ( Partial_Sums ((seq ^\ k) ^\ 1)) = ((( Partial_Sums (seq ^\ k)) ^\ 1) - seq1) by Th12;

        then (seq ^\ (k + 1)) = ((seq ^\ k) ^\ 1) & ( Partial_Sums ((seq ^\ k) ^\ 1)) is convergent by A2, BHSP_2: 4, BHSP_3: 31;

        hence thesis by Def2;

      end;

      assume seq is summable;

      then

       A3: P[ 0 ] by NAT_1: 47;

      thus for k holds P[k] from NAT_1:sch 2( A3, A1);

    end;

    theorem :: BHSP_4:14

    (ex k st (seq ^\ k) is summable) implies seq is summable

    proof

      given k such that

       A1: (seq ^\ k) is summable;

      ((seq ^\ k) ^\ 1) is summable by A1, Th13;

      then

       A2: ( Partial_Sums ((seq ^\ k) ^\ 1)) is convergent;

      reconsider seq1 = ( NAT --> (( Partial_Sums seq) . k)) as sequence of X;

      defpred P[ Nat] means ((( Partial_Sums seq) ^\ (k + 1)) . $1) = ((( Partial_Sums (seq ^\ (k + 1))) . $1) + (seq1 . $1));



       A3: (( Partial_Sums (seq ^\ (k + 1))) . 0 ) = ((seq ^\ (k + 1)) . 0 ) by Def1

      .= (seq . ( 0 + (k + 1))) by NAT_1:def 3

      .= (seq . (k + 1));

       A4:

      now

        let m;



         A5: m in NAT by ORDINAL1:def 12;

        assume

         A6: P[m];

        ((( Partial_Sums (seq ^\ (k + 1))) . (m + 1)) + (seq1 . (m + 1))) = ((seq1 . (m + 1)) + ((( Partial_Sums (seq ^\ (k + 1))) . m) + ((seq ^\ (k + 1)) . (m + 1)))) by Def1

        .= (((seq1 . (m + 1)) + (( Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1))) by RLVECT_1:def 3

        .= (((( Partial_Sums seq) . k) + (( Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1)))

        .= (((( Partial_Sums seq) ^\ (k + 1)) . m) + ((seq ^\ (k + 1)) . (m + 1))) by A6, FUNCOP_1: 7, A5

        .= ((( Partial_Sums seq) . (m + (k + 1))) + ((seq ^\ (k + 1)) . (m + 1))) by NAT_1:def 3

        .= ((( Partial_Sums seq) . (m + (k + 1))) + (seq . ((m + 1) + (k + 1)))) by NAT_1:def 3

        .= (( Partial_Sums seq) . ((m + (k + 1)) + 1)) by Def1

        .= (( Partial_Sums seq) . ((m + 1) + (k + 1)))

        .= ((( Partial_Sums seq) ^\ (k + 1)) . (m + 1)) by NAT_1:def 3;

        hence P[(m + 1)];

      end;

      ((( Partial_Sums seq) ^\ (k + 1)) . 0 ) = (( Partial_Sums seq) . ( 0 + (k + 1))) by NAT_1:def 3

      .= ((( Partial_Sums seq) . k) + (seq . (k + 1))) by Def1

      .= ((( Partial_Sums (seq ^\ (k + 1))) . 0 ) + (seq1 . 0 )) by A3;

      then

       A7: P[ 0 ];

      for m holds P[m] from NAT_1:sch 2( A7, A4);



      then

       A8: (( Partial_Sums seq) ^\ (k + 1)) = (( Partial_Sums (seq ^\ (k + 1))) + seq1) by NORMSP_1:def 2

      .= (( Partial_Sums ((seq ^\ k) ^\ 1)) + seq1) by BHSP_3: 31;

      (( Partial_Sums seq) ^\ (k + 1)) is convergent by A2, A8, BHSP_2: 3;

      hence thesis by BHSP_3: 37;

    end;

    definition

      let X, seq, n;

      :: BHSP_4:def4

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

      coherence ;

    end

    theorem :: BHSP_4:15

    ( Sum (seq, 0 )) = (seq . 0 ) by Def1;

    theorem :: BHSP_4:16



     Th16: ( Sum (seq,1)) = (( Sum (seq, 0 )) + (seq . 1))

    proof

      (( Partial_Sums seq) . 1) = ((( Partial_Sums seq) . 0 ) + (seq . ( 0 + 1))) by Def1

      .= ((( Partial_Sums seq) . 0 ) + (seq . 1));

      hence thesis;

    end;

    theorem :: BHSP_4:17



     Th17: ( Sum (seq,1)) = ((seq . 0 ) + (seq . 1))

    proof



      thus ( Sum (seq,1)) = (( Sum (seq, 0 )) + (seq . 1)) by Th16

      .= ((seq . 0 ) + (seq . 1)) by Def1;

    end;

    theorem :: BHSP_4:18

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

    theorem :: BHSP_4:19



     Th19: (seq . (n + 1)) = (( Sum (seq,(n + 1))) - ( Sum (seq,n)))

    proof



      thus (( Sum (seq,(n + 1))) - ( Sum (seq,n))) = (((seq . (n + 1)) + ( Sum (seq,n))) - ( Sum (seq,n))) by Def1

      .= ((seq . (n + 1)) + (( Sum (seq,n)) - ( Sum (seq,n)))) by RLVECT_1:def 3

      .= ((seq . (n + 1)) + ( 0. X)) by RLVECT_1: 15

      .= (seq . (n + 1));

    end;

    theorem :: BHSP_4:20

    (seq . 1) = (( Sum (seq,1)) - ( Sum (seq, 0 )))

    proof

      (seq . ( 0 + 1)) = (( Sum (seq,( 0 + 1))) - ( Sum (seq, 0 ))) by Th19;

      hence thesis;

    end;

    definition

      let X, seq, n, m;

      :: BHSP_4:def5

      func Sum (seq,n,m) -> Point of X equals (( Sum (seq,n)) - ( Sum (seq,m)));

      coherence ;

    end

    theorem :: BHSP_4:21

    ( Sum (seq,1, 0 )) = (seq . 1)

    proof

      ( Sum (seq,1, 0 )) = (((seq . 0 ) + (seq . 1)) - ( Sum (seq, 0 ))) by Th17

      .= (((seq . 1) + (seq . 0 )) - (seq . 0 )) by Def1

      .= ((seq . 1) + ((seq . 0 ) - (seq . 0 ))) by RLVECT_1:def 3

      .= ((seq . 1) + 09(X)) by RLVECT_1: 15;

      hence thesis;

    end;

    theorem :: BHSP_4:22

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

    theorem :: BHSP_4:23



     Th23: for X be RealHilbertSpace, seq be sequence of X holds seq is summable iff for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r

    proof

      let X be RealHilbertSpace, seq be sequence of X;

      thus seq is summable implies for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r

      proof

        assume

         A1: seq is summable;

        now

          let r;

          assume r > 0 ;

          then

          consider k such that

           A2: for n, m st n >= k & m >= k holds ||.((( Partial_Sums seq) . n) - (( Partial_Sums seq) . m)).|| < r by A1, Th10;

          take k;

          let n, m;

          assume n >= k & m >= k;

          hence ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r by A2;

        end;

        hence thesis;

      end;

      thus (for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r) implies seq is summable

      proof

        assume

         A3: for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r;

        now

          let r;

          assume r > 0 ;

          then

          consider k such that

           A4: for n, m st n >= k & m >= k holds ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r by A3;

          take k;

          let n, m;

          assume n >= k & m >= k;

          then ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r by A4;

          hence ||.((( Partial_Sums seq) . n) - (( Partial_Sums seq) . m)).|| < r;

        end;

        hence thesis by Th10;

      end;

    end;

    theorem :: BHSP_4:24

    for X be RealHilbertSpace, seq be sequence of X holds seq is summable iff for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.( Sum (seq,n,m)).|| < r

    proof

      let X be RealHilbertSpace, seq be sequence of X;

      thus seq is summable implies for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.( Sum (seq,n,m)).|| < r

      proof

        assume

         A1: seq is summable;

        now

          let r;

          assume r > 0 ;

          then

          consider k such that

           A2: for n, m st n >= k & m >= k holds ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r by A1, Th23;

          take k;

          let n, m;

          assume n >= k & m >= k;

          hence ||.( Sum (seq,n,m)).|| < r by A2;

        end;

        hence thesis;

      end;

      thus (for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.( Sum (seq,n,m)).|| < r) implies seq is summable

      proof

        assume

         A3: for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.( Sum (seq,n,m)).|| < r;

        now

          let r;

          assume r > 0 ;

          then

          consider k such that

           A4: for n, m st n >= k & m >= k holds ||.( Sum (seq,n,m)).|| < r by A3;

          take k;

          let n, m;

          assume n >= k & m >= k;

          then ||.( Sum (seq,n,m)).|| < r by A4;

          hence ||.(( Sum (seq,n)) - ( Sum (seq,m))).|| < r;

        end;

        hence thesis by Th23;

      end;

    end;

    definition

      let X, seq;

      :: BHSP_4:def6

      attr seq is absolutely_summable means ||.seq.|| is summable;

    end

    theorem :: BHSP_4:25

    seq1 is absolutely_summable & seq2 is absolutely_summable implies (seq1 + seq2) is absolutely_summable

    proof



       A1: for n be Nat holds ( ||.(seq1 + seq2).|| . n) >= 0 & ( ||.(seq1 + seq2).|| . n) <= (( ||.seq1.|| + ||.seq2.||) . n)

      proof

        let n be Nat;

        ( ||.(seq1 + seq2).|| . n) = ||.((seq1 + seq2) . n).|| by BHSP_2:def 3;

        hence ( ||.(seq1 + seq2).|| . n) >= 0 by BHSP_1: 28;

        ( ||.(seq1 + seq2).|| . n) = ||.((seq1 + seq2) . n).|| by BHSP_2:def 3

        .= ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def 2;

        then ( ||.(seq1 + seq2).|| . n) <= ( ||.(seq1 . n).|| + ||.(seq2 . n).||) by BHSP_1: 30;

        then ( ||.(seq1 + seq2).|| . n) <= (( ||.seq1.|| . n) + ||.(seq2 . n).||) by BHSP_2:def 3;

        then ( ||.(seq1 + seq2).|| . n) <= (( ||.seq1.|| . n) + ( ||.seq2.|| . n)) by BHSP_2:def 3;

        hence ( ||.(seq1 + seq2).|| . n) <= (( ||.seq1.|| + ||.seq2.||) . n) by SEQ_1: 7;

      end;

      assume seq1 is absolutely_summable & seq2 is absolutely_summable;

      then ||.seq1.|| is summable & ||.seq2.|| is summable;

      then ( ||.seq1.|| + ||.seq2.||) is summable by SERIES_1: 7;

      then ||.(seq1 + seq2).|| is summable by A1, SERIES_1: 20;

      hence thesis;

    end;

    theorem :: BHSP_4:26

    seq is absolutely_summable implies (a * seq) is absolutely_summable

    proof



       A1: for n be Nat holds ( ||.(a * seq).|| . n) >= 0 & ( ||.(a * seq).|| . n) <= (( |.a.| (#) ||.seq.||) . n)

      proof

        let n be Nat;

        ( ||.(a * seq).|| . n) = ||.((a * seq) . n).|| by BHSP_2:def 3;

        hence ( ||.(a * seq).|| . n) >= 0 by BHSP_1: 28;

        ( ||.(a * seq).|| . n) = ||.((a * seq) . n).|| by BHSP_2:def 3

        .= ||.(a * (seq . n)).|| by NORMSP_1:def 5

        .= ( |.a.| * ||.(seq . n).||) by BHSP_1: 27

        .= ( |.a.| * ( ||.seq.|| . n)) by BHSP_2:def 3

        .= (( |.a.| (#) ||.seq.||) . n) by SEQ_1: 9;

        hence ( ||.(a * seq).|| . n) <= (( |.a.| (#) ||.seq.||) . n);

      end;

      assume seq is absolutely_summable;

      then ||.seq.|| is summable;

      then ( |.a.| (#) ||.seq.||) is summable by SERIES_1: 10;

      then ||.(a * seq).|| is summable by A1, SERIES_1: 20;

      hence thesis;

    end;

    theorem :: BHSP_4:27

    (for n be Nat holds ( ||.seq.|| . n) <= (Rseq . n)) & Rseq is summable implies seq is absolutely_summable

    proof



       A1: for n be Nat holds ( ||.seq.|| . n) >= 0

      proof

        let n be Nat;

        ( ||.seq.|| . n) = ||.(seq . n).|| by BHSP_2:def 3;

        hence thesis by BHSP_1: 28;

      end;

      assume (for n be Nat holds ( ||.seq.|| . n) <= (Rseq . n)) & Rseq is summable;

      then ||.seq.|| is summable by A1, SERIES_1: 20;

      hence thesis;

    end;

    theorem :: BHSP_4:28

    (for n be Nat holds (seq . n) <> ( 0. X) & (Rseq . n) = ( ||.(seq . (n + 1)).|| / ||.(seq . n).||)) & Rseq is convergent & ( lim Rseq) < 1 implies seq is absolutely_summable

    proof

      assume that

       A1: for n be Nat holds (seq . n) <> 09(X) & (Rseq . n) = ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) and

       A2: Rseq is convergent & ( lim Rseq) < 1;

      for n be Nat holds ( ||.seq.|| . n) > 0 & (Rseq . n) = (( ||.seq.|| . (n + 1)) / ( ||.seq.|| . n))

      proof

        let n be Nat;



         A3: ||.(seq . n).|| <> 0 by A1, BHSP_1: 26;

         ||.(seq . n).|| >= 0 by BHSP_1: 28;

        hence ( ||.seq.|| . n) > 0 by A3, BHSP_2:def 3;

        (Rseq . n) = ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) by A1

        .= (( ||.seq.|| . (n + 1)) / ||.(seq . n).||) by BHSP_2:def 3;

        hence (Rseq . n) = (( ||.seq.|| . (n + 1)) / ( ||.seq.|| . n)) by BHSP_2:def 3;

      end;

      hence thesis by A2, SERIES_1: 26;

    end;

    theorem :: BHSP_4:29



     Th29: r > 0 & (ex m st for n st n >= m holds ||.(seq . n).|| >= r) implies not seq is convergent or ( lim seq) <> ( 0. X)

    proof

      assume

       A1: r > 0 ;

      given m such that

       A2: for n st n >= m holds ||.(seq . n).|| >= r;

      per cases ;

        suppose not seq is convergent;

        hence thesis;

      end;

        suppose

         A3: seq is convergent;

        now

          assume ( lim seq) = 09(X);

          then

          consider k be Nat such that

           A4: for n be Nat st n >= k holds ||.((seq . n) - 09(X)).|| < r by A1, A3, BHSP_2: 19;

          set n = (m + k);

          (m + k) >= k by NAT_1: 11;

          then n >= k;

          then ||.((seq . n) - 09(X)).|| < r by A4;

          then

           A5: ||.(seq . n).|| < r;

          (m + k) >= m by NAT_1: 11;

          then n >= m;

          hence contradiction by A2, A5;

        end;

        hence thesis;

      end;

    end;

    theorem :: BHSP_4:30



     Th30: (for n holds (seq . n) <> ( 0. X)) & (ex m st for n st n >= m holds ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) >= 1) implies not seq is summable

    proof

      assume

       A1: for n holds (seq . n) <> 09(X);

      given m such that

       A2: for n st n >= m holds ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) >= 1;

       A3:

      now

        defpred P[ Nat] means ||.(seq . (m + $1)).|| >= ||.(seq . m).||;

        let n;



         A4: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume

           A5: ||.(seq . (m + k)).|| >= ||.(seq . m).||;



           A6: ||.(seq . (m + k)).|| <> 0 by A1, BHSP_1: 26;

          ( ||.(seq . ((m + k) + 1)).|| / ||.(seq . (m + k)).||) >= 1 & ||.(seq . (m + k)).|| >= 0 by A2, BHSP_1: 28, NAT_1: 11;

          then ||.(seq . ((m + k) + 1)).|| >= ||.(seq . (m + k)).|| by A6, XREAL_1: 191;

          hence thesis by A5, XXREAL_0: 2;

        end;



         A7: P[ 0 ];



         A8: for k holds P[k] from NAT_1:sch 2( A7, A4);

        assume n >= m;

        then

        consider k be Nat such that

         A9: n = (m + k) by NAT_1: 10;

        thus ||.(seq . n).|| >= ||.(seq . m).|| by A8, A9;

      end;



       A10: ||.(seq . m).|| <> 0 by A1, BHSP_1: 26;

       ||.(seq . m).|| >= 0 by BHSP_1: 28;

      then not seq is convergent or ( lim seq) <> 09(X) by A10, A3, Th29;

      hence thesis by Th9;

    end;

    theorem :: BHSP_4:31

    (for n holds (seq . n) <> ( 0. X)) & (for n holds (Rseq . n) = ( ||.(seq . (n + 1)).|| / ||.(seq . n).||)) & Rseq is convergent & ( lim Rseq) > 1 implies not seq is summable

    proof

      assume that

       A1: for n holds (seq . n) <> 09(X) and

       A2: for n holds (Rseq . n) = ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) and

       A3: Rseq is convergent and

       A4: ( lim Rseq) > 1;

      (( lim Rseq) - 1) > 0 by A4, XREAL_1: 50;

      then

      consider m be Nat such that

       A5: for n be Nat st n >= m holds |.((Rseq . n) - ( lim Rseq)).| < (( lim Rseq) - 1) by A3, SEQ_2:def 7;

      now

        let n;



         A6: (m + 1) >= m by NAT_1: 11;



         A7: (Rseq . n) = ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) by A2;

        assume n >= (m + 1);

        then n >= m by A6, XXREAL_0: 2;

        then |.(( ||.(seq . (n + 1)).|| / ||.(seq . n).||) - ( lim Rseq)).| < (( lim Rseq) - 1) by A5, A7;

        then ( - (( lim Rseq) - 1)) < (( ||.(seq . (n + 1)).|| / ||.(seq . n).||) - ( lim Rseq)) by SEQ_2: 1;

        then ((1 - ( lim Rseq)) + ( lim Rseq)) < ((( ||.(seq . (n + 1)).|| / ||.(seq . n).||) - ( lim Rseq)) + ( lim Rseq)) by XREAL_1: 6;

        hence ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) >= 1;

      end;

      hence thesis by A1, Th30;

    end;

    theorem :: BHSP_4:32

    (for n holds (Rseq . n) = (n -root ||.(seq . n).||)) & Rseq is convergent & ( lim Rseq) < 1 implies seq is absolutely_summable

    proof

      assume that

       A1: for n holds (Rseq . n) = (n -root ||.(seq . n).||) and

       A2: Rseq is convergent & ( lim Rseq) < 1;

      for n be Nat holds ( ||.seq.|| . n) >= 0 & (Rseq . n) = (n -root ( ||.seq.|| . n))

      proof

        let n be Nat;

        ( ||.seq.|| . n) = ||.(seq . n).|| by BHSP_2:def 3;

        hence ( ||.seq.|| . n) >= 0 by BHSP_1: 28;

        (Rseq . n) = (n -root ||.(seq . n).||) by A1;

        hence (Rseq . n) = (n -root ( ||.seq.|| . n)) by BHSP_2:def 3;

      end;

      hence thesis by A2, SERIES_1: 28;

    end;

    theorem :: BHSP_4:33

    (for n holds (Rseq . n) = (n -root ( ||.seq.|| . n))) & (ex m st for n st n >= m holds (Rseq . n) >= 1) implies not seq is summable

    proof

      assume

       A1: for n holds (Rseq . n) = (n -root ( ||.seq.|| . n));

      given m such that

       A2: for n st n >= m holds (Rseq . n) >= 1;

      now

        let n;

        assume

         A3: n >= (m + 1);

        (m + 1) >= 1 by NAT_1: 11;

        then

         A4: n >= 1 by A3, XXREAL_0: 2;

        (m + 1) >= m by NAT_1: 11;

        then

         A5: n >= m by A3, XXREAL_0: 2;

        (Rseq . n) = (n -root ( ||.seq.|| . n)) by A1

        .= (n -root ||.(seq . n).||) by BHSP_2:def 3;

        then ||.(seq . n).|| >= 0 & ((n -root ||.(seq . n).||) |^ n) >= 1 by A2, A5, BHSP_1: 28, PREPOWER: 11;

        hence ||.(seq . n).|| >= 1 by A4, POWER: 4;

      end;

      then not seq is convergent or ( lim seq) <> 09(X) by Th29;

      hence thesis by Th9;

    end;

    theorem :: BHSP_4:34

    (for n holds (Rseq . n) = (n -root ( ||.seq.|| . n))) & Rseq is convergent & ( lim Rseq) > 1 implies not seq is summable

    proof

      assume that

       A1: for n holds (Rseq . n) = (n -root ( ||.seq.|| . n)) and

       A2: Rseq is convergent and

       A3: ( lim Rseq) > 1;

      (( lim Rseq) - 1) > 0 by A3, XREAL_1: 50;

      then

      consider m be Nat such that

       A4: for n be Nat st n >= m holds |.((Rseq . n) - ( lim Rseq)).| < (( lim Rseq) - 1) by A2, SEQ_2:def 7;

      now

        let n;

        assume

         A5: n >= (m + 1);



         A6: (Rseq . n) = (n -root ( ||.seq.|| . n)) by A1

        .= (n -root ||.(seq . n).||) by BHSP_2:def 3;

        (m + 1) >= m by NAT_1: 11;

        then n >= m by A5, XXREAL_0: 2;

        then |.((n -root ||.(seq . n).||) - ( lim Rseq)).| < (( lim Rseq) - 1) by A4, A6;

        then ( - (( lim Rseq) - 1)) < ((n -root ||.(seq . n).||) - ( lim Rseq)) by SEQ_2: 1;

        then ((1 - ( lim Rseq)) + ( lim Rseq)) < (((n -root ||.(seq . n).||) - ( lim Rseq)) + ( lim Rseq)) by XREAL_1: 6;

        then

         A7: ||.(seq . n).|| >= 0 & ((n -root ||.(seq . n).||) |^ n) >= 1 by BHSP_1: 28, PREPOWER: 11;

        (m + 1) >= 1 by NAT_1: 11;

        then n >= 1 by A5, XXREAL_0: 2;

        hence ||.(seq . n).|| >= 1 by A7, POWER: 4;

      end;

      then not seq is convergent or ( lim seq) <> 09(X) by Th29;

      hence thesis by Th9;

    end;

    theorem :: BHSP_4:35



     Th35: ( Partial_Sums ||.seq.||) is non-decreasing

    proof

      now

        let n be Nat;

         ||.(seq . (n + 1)).|| >= 0 by BHSP_1: 28;

        then ( ||.seq.|| . (n + 1)) >= 0 by BHSP_2:def 3;

        then ( 0 + (( Partial_Sums ||.seq.||) . n)) <= (( ||.seq.|| . (n + 1)) + (( Partial_Sums ||.seq.||) . n)) by XREAL_1: 6;

        hence (( Partial_Sums ||.seq.||) . n) <= (( Partial_Sums ||.seq.||) . (n + 1)) by SERIES_1:def 1;

      end;

      hence thesis;

    end;

    theorem :: BHSP_4:36

    for n holds (( Partial_Sums ||.seq.||) . n) >= 0

    proof

      let n;

       ||.(seq . 0 ).|| >= 0 by BHSP_1: 28;

      then

       A1: ( ||.seq.|| . 0 ) >= 0 by BHSP_2:def 3;

      (( Partial_Sums ||.seq.||) . 0 ) <= (( Partial_Sums ||.seq.||) . n) by Th35, SEQM_3: 11;

      hence thesis by A1, SERIES_1:def 1;

    end;

    theorem :: BHSP_4:37



     Th37: for n holds ||.(( Partial_Sums seq) . n).|| <= (( Partial_Sums ||.seq.||) . n)

    proof

      defpred P[ Nat] means ||.(( Partial_Sums seq) . $1).|| <= (( Partial_Sums ||.seq.||) . $1);

       A1:

      now

        let n;

        assume P[n];

        then

         A2: ( ||.(( Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).||) <= ((( Partial_Sums ||.seq.||) . n) + ||.(seq . (n + 1)).||) by XREAL_1: 6;

        (( Partial_Sums seq) . (n + 1)) = ((( Partial_Sums seq) . n) + (seq . (n + 1))) by Def1;

        then ||.(( Partial_Sums seq) . (n + 1)).|| <= ( ||.(( Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).||) by BHSP_1: 30;

        then ||.(( Partial_Sums seq) . (n + 1)).|| <= ((( Partial_Sums ||.seq.||) . n) + ||.(seq . (n + 1)).||) by A2, XXREAL_0: 2;

        then ||.(( Partial_Sums seq) . (n + 1)).|| <= ((( Partial_Sums ||.seq.||) . n) + ( ||.seq.|| . (n + 1))) by BHSP_2:def 3;

        hence P[(n + 1)] by SERIES_1:def 1;

      end;

      (( Partial_Sums ||.seq.||) . 0 ) = ( ||.seq.|| . 0 ) by SERIES_1:def 1

      .= ||.(seq . 0 ).|| by BHSP_2:def 3;

      then

       A3: P[ 0 ] by Def1;

      thus for n holds P[n] from NAT_1:sch 2( A3, A1);

    end;

    theorem :: BHSP_4:38

    for n holds ||.( Sum (seq,n)).|| <= ( Sum ( ||.seq.||,n)) by Th37;

    theorem :: BHSP_4:39



     Th39: for n, m holds ||.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).|| <= |.((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . n)).|

    proof

      let n, m;

       A1:

      now

        reconsider d = n, t = m as Integer;

        set PSseq9 = ( Partial_Sums ||.seq.||);

        set PSseq = ( Partial_Sums seq);

        defpred P[ Nat] means ||.((PSseq . m) - (PSseq . (m + $1))).|| <= |.((PSseq9 . m) - (PSseq9 . (m + $1))).|;



         A2: PSseq9 is non-decreasing by Th35;

         A3:

        now

          let k;



           A4: ||.(seq . ((m + k) + 1)).|| >= 0 by BHSP_1: 28;



           A5: |.((PSseq9 . m) - (PSseq9 . (m + (k + 1)))).| = |.( - ((PSseq9 . (m + (k + 1))) - (PSseq9 . m))).|

          .= |.((PSseq9 . ((m + k) + 1)) - (PSseq9 . m)).| by COMPLEX1: 52

          .= |.(((PSseq9 . (m + k)) + ( ||.seq.|| . ((m + k) + 1))) - (PSseq9 . m)).| by SERIES_1:def 1

          .= |.(( ||.(seq . ((m + k) + 1)).|| + (PSseq9 . (m + k))) - (PSseq9 . m)).| by BHSP_2:def 3

          .= |.(((PSseq9 . (m + k)) - (PSseq9 . m)) + ||.(seq . ((m + k) + 1)).||).|;

           ||.((PSseq . m) - (PSseq . (m + (k + 1)))).|| = ||.((PSseq . m) - ((PSseq . (m + k)) + (seq . ((m + k) + 1)))).|| by Def1

          .= ||.(((PSseq . m) - (PSseq . (m + k))) - (seq . ((m + k) + 1))).|| by RLVECT_1: 27

          .= ||.(((PSseq . m) - (PSseq . (m + k))) + ( - (seq . ((m + k) + 1)))).||;

          then ||.((PSseq . m) - (PSseq . (m + (k + 1)))).|| <= ( ||.((PSseq . m) - (PSseq . (m + k))).|| + ||.( - (seq . ((m + k) + 1))).||) by BHSP_1: 30;

          then

           A6: ||.((PSseq . m) - (PSseq . (m + (k + 1)))).|| <= ( ||.((PSseq . m) - (PSseq . (m + k))).|| + ||.(seq . ((m + k) + 1)).||) by BHSP_1: 31;



           A7: ((PSseq9 . (m + k)) - (PSseq9 . m)) >= 0 by A2, SEQM_3: 5, XREAL_1: 48;

          assume P[k];

          then ( ||.((PSseq . m) - (PSseq . (m + k))).|| + ||.(seq . ((m + k) + 1)).||) <= ( |.((PSseq9 . m) - (PSseq9 . (m + k))).| + ||.(seq . ((m + k) + 1)).||) by XREAL_1: 6;

          then ||.((PSseq . m) - (PSseq . (m + (k + 1)))).|| <= ( |.( - ((PSseq9 . (m + k)) - (PSseq9 . m))).| + ||.(seq . ((m + k) + 1)).||) by A6, XXREAL_0: 2;

          then ||.((PSseq . m) - (PSseq . (m + (k + 1)))).|| <= ( |.((PSseq9 . (m + k)) - (PSseq9 . m)).| + ||.(seq . ((m + k) + 1)).||) by COMPLEX1: 52;

          then ||.((PSseq . m) - (PSseq . (m + (k + 1)))).|| <= (((PSseq9 . (m + k)) - (PSseq9 . m)) + ||.(seq . ((m + k) + 1)).||) by A7, ABSVALUE:def 1;

          hence P[(k + 1)] by A7, A4, A5, ABSVALUE:def 1;

        end;

        assume n >= m;

        then

        reconsider k = (d - t) as Element of NAT by INT_1: 5;



         A8: (m + k) = n;

         ||.((PSseq . m) - (PSseq . (m + 0 ))).|| = ||. 09(X).|| by RLVECT_1: 15

        .= 0 by BHSP_1: 26;

        then

         A9: P[ 0 ] by COMPLEX1: 46;

        for k holds P[k] from NAT_1:sch 2( A9, A3);

        hence thesis by A8;

      end;

      now

        reconsider d = n, t = m as Integer;

        set PSseq9 = ( Partial_Sums ||.seq.||);

        set PSseq = ( Partial_Sums seq);

        defpred P[ Nat] means ||.((PSseq . (n + $1)) - (PSseq . n)).|| <= |.((PSseq9 . (n + $1)) - (PSseq9 . n)).|;



         A10: PSseq9 is non-decreasing by Th35;

         A11:

        now

          let k;



           A12: ||.(seq . ((n + k) + 1)).|| >= 0 by BHSP_1: 28;



           A13: |.((PSseq9 . (n + (k + 1))) - (PSseq9 . n)).| = |.(((PSseq9 . (n + k)) + ( ||.seq.|| . ((n + k) + 1))) - (PSseq9 . n)).| by SERIES_1:def 1

          .= |.(( ||.(seq . ((n + k) + 1)).|| + (PSseq9 . (n + k))) - (PSseq9 . n)).| by BHSP_2:def 3

          .= |.( ||.(seq . ((n + k) + 1)).|| + ((PSseq9 . (n + k)) - (PSseq9 . n))).|;

          assume P[k];

          then

           A14: ( ||.(seq . ((n + k) + 1)).|| + ||.((PSseq . (n + k)) - (PSseq . n)).||) <= ( ||.(seq . ((n + k) + 1)).|| + |.((PSseq9 . (n + k)) - (PSseq9 . n)).|) by XREAL_1: 7;



           A15: ((PSseq9 . (n + k)) - (PSseq9 . n)) >= 0 by A10, SEQM_3: 5, XREAL_1: 48;

           ||.((PSseq . (n + (k + 1))) - (PSseq . n)).|| = ||.(((seq . ((n + k) + 1)) + (PSseq . (n + k))) - (PSseq . n)).|| by Def1

          .= ||.((seq . ((n + k) + 1)) + ((PSseq . (n + k)) - (PSseq . n))).|| by RLVECT_1:def 3;

          then ||.((PSseq . (n + (k + 1))) - (PSseq . n)).|| <= ( ||.(seq . ((n + k) + 1)).|| + ||.((PSseq . (n + k)) - (PSseq . n)).||) by BHSP_1: 30;

          then ||.((PSseq . (n + (k + 1))) - (PSseq . n)).|| <= ( ||.(seq . ((n + k) + 1)).|| + |.((PSseq9 . (n + k)) - (PSseq9 . n)).|) by A14, XXREAL_0: 2;

          then ||.((PSseq . (n + (k + 1))) - (PSseq . n)).|| <= ( ||.(seq . ((n + k) + 1)).|| + ((PSseq9 . (n + k)) - (PSseq9 . n))) by A15, ABSVALUE:def 1;

          hence P[(k + 1)] by A15, A12, A13, ABSVALUE:def 1;

        end;

        assume n <= m;

        then

        reconsider k = (t - d) as Element of NAT by INT_1: 5;



         A16: (n + k) = m;

         ||.((PSseq . (n + 0 )) - (PSseq . n)).|| = ||. 09(X).|| by RLVECT_1: 15

        .= 0 by BHSP_1: 26;

        then

         A17: P[ 0 ] by COMPLEX1: 46;

        for k holds P[k] from NAT_1:sch 2( A17, A11);

        hence thesis by A16;

      end;

      hence thesis by A1;

    end;

    theorem :: BHSP_4:40

    for n, m holds ||.(( Sum (seq,m)) - ( Sum (seq,n))).|| <= |.(( Sum ( ||.seq.||,m)) - ( Sum ( ||.seq.||,n))).| by Th39;

    theorem :: BHSP_4:41

    for n, m holds ||.( Sum (seq,m,n)).|| <= |.( Sum ( ||.seq.||,m,n)).| by Th39;

    theorem :: BHSP_4:42

    for X be RealHilbertSpace, seq be sequence of X holds seq is absolutely_summable implies seq is summable

    proof

      let X be RealHilbertSpace, seq be sequence of X;

      assume that

       A1: seq is absolutely_summable;



       A2: ||.seq.|| is summable by A1;

      now

        let r;

        assume r > 0 ;

        then

        consider k be Nat such that

         A3: for m be Nat st m >= k holds |.((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . k)).| < (r / 2) by A2, SERIES_1: 21, XREAL_1: 215;

        reconsider k as Nat;

        take k;

        now

          let m, n;



           A4: ||.((( Partial_Sums seq) . n) - (( Partial_Sums seq) . m)).|| <= |.((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . m)).| by Th39;

          assume m >= k & n >= k;

          then |.((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . k)).| < (r / 2) & |.((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . k)).| < (r / 2) by A3;

          then

           A5: ( |.((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . k)).| + |.((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . k)).|) < ((r / 2) + (r / 2)) by XREAL_1: 8;

           |.((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . m)).| = |.(((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . k)) - ((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . k))).|;

          then |.((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . m)).| <= ( |.((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . k)).| + |.((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . k)).|) by COMPLEX1: 57;

          then |.((( Partial_Sums ||.seq.||) . n) - (( Partial_Sums ||.seq.||) . m)).| < r by A5, XXREAL_0: 2;

          hence ||.((( Partial_Sums seq) . n) - (( Partial_Sums seq) . m)).|| < r by A4, XXREAL_0: 2;

        end;

        hence for n, m st n >= k & m >= k holds ||.((( Partial_Sums seq) . n) - (( Partial_Sums seq) . m)).|| < r;

      end;

      hence thesis by Th10;

    end;

    definition

      let X, seq, Rseq;

      :: BHSP_4:def7

      func Rseq * seq -> sequence of X means

      : Def7: for n holds (it . n) = ((Rseq . n) * (seq . n));

      existence

      proof

        deffunc F( Nat) = ((Rseq . $1) * (seq . $1));

        consider M be sequence of X such that

         A1: for n be Element of NAT holds (M . n) = F(n) from FUNCT_2:sch 4;

        take M;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let seq1, seq2;

        assume that

         A2: for n holds (seq1 . n) = ((Rseq . n) * (seq . n)) and

         A3: for n holds (seq2 . n) = ((Rseq . n) * (seq . n));

        let n be Element of NAT ;

        (seq1 . n) = ((Rseq . n) * (seq . n)) by A2;

        hence (seq1 . n) = (seq2 . n) by A3;

      end;

    end

    theorem :: BHSP_4:43

    (Rseq * (seq1 + seq2)) = ((Rseq * seq1) + (Rseq * seq2))

    proof

      let n be Element of NAT ;



      thus ((Rseq * (seq1 + seq2)) . n) = ((Rseq . n) * ((seq1 + seq2) . n)) by Def7

      .= ((Rseq . n) * ((seq1 . n) + (seq2 . n))) by NORMSP_1:def 2

      .= (((Rseq . n) * (seq1 . n)) + ((Rseq . n) * (seq2 . n))) by RLVECT_1:def 5

      .= (((Rseq * seq1) . n) + ((Rseq . n) * (seq2 . n))) by Def7

      .= (((Rseq * seq1) . n) + ((Rseq * seq2) . n)) by Def7

      .= (((Rseq * seq1) + (Rseq * seq2)) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_4:44

    ((Rseq1 + Rseq2) * seq) = ((Rseq1 * seq) + (Rseq2 * seq))

    proof

      let n be Element of NAT ;



      thus (((Rseq1 + Rseq2) * seq) . n) = (((Rseq1 + Rseq2) . n) * (seq . n)) by Def7

      .= (((Rseq1 . n) + (Rseq2 . n)) * (seq . n)) by SEQ_1: 7

      .= (((Rseq1 . n) * (seq . n)) + ((Rseq2 . n) * (seq . n))) by RLVECT_1:def 6

      .= (((Rseq1 * seq) . n) + ((Rseq2 . n) * (seq . n))) by Def7

      .= (((Rseq1 * seq) . n) + ((Rseq2 * seq) . n)) by Def7

      .= (((Rseq1 * seq) + (Rseq2 * seq)) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_4:45

    ((Rseq1 (#) Rseq2) * seq) = (Rseq1 * (Rseq2 * seq))

    proof

      let n be Element of NAT ;



      thus (((Rseq1 (#) Rseq2) * seq) . n) = (((Rseq1 (#) Rseq2) . n) * (seq . n)) by Def7

      .= (((Rseq1 . n) * (Rseq2 . n)) * (seq . n)) by SEQ_1: 8

      .= ((Rseq1 . n) * ((Rseq2 . n) * (seq . n))) by RLVECT_1:def 7

      .= ((Rseq1 . n) * ((Rseq2 * seq) . n)) by Def7

      .= ((Rseq1 * (Rseq2 * seq)) . n) by Def7;

    end;

    theorem :: BHSP_4:46



     Th46: ((a (#) Rseq) * seq) = (a * (Rseq * seq))

    proof

      let n be Element of NAT ;



      thus (((a (#) Rseq) * seq) . n) = (((a (#) Rseq) . n) * (seq . n)) by Def7

      .= ((a * (Rseq . n)) * (seq . n)) by SEQ_1: 9

      .= (a * ((Rseq . n) * (seq . n))) by RLVECT_1:def 7

      .= (a * ((Rseq * seq) . n)) by Def7

      .= ((a * (Rseq * seq)) . n) by NORMSP_1:def 5;

    end;

    theorem :: BHSP_4:47

    (Rseq * ( - seq)) = (( - Rseq) * seq)

    proof

      let n be Element of NAT ;



      thus ((Rseq * ( - seq)) . n) = ((Rseq . n) * (( - seq) . n)) by Def7

      .= ((Rseq . n) * ( - (seq . n))) by BHSP_1: 44

      .= (( - (Rseq . n)) * (seq . n)) by RLVECT_1: 24

      .= ((( - Rseq) . n) * (seq . n)) by SEQ_1: 10

      .= ((( - Rseq) * seq) . n) by Def7;

    end;

    theorem :: BHSP_4:48



     Th48: Rseq is convergent & seq is convergent implies (Rseq * seq) is convergent

    proof

      assume that

       A1: Rseq is convergent and

       A2: seq is convergent;

      consider p be Real such that

       A3: for r be Real st r > 0 holds ex m be Nat st for n be Nat st n >= m holds |.((Rseq . n) - p).| < r by A1, SEQ_2:def 6;

      consider g such that

       A4: for r st r > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((seq . n) - g).|| < r by A2, BHSP_2: 9;

      reconsider p as Real;

      now

        take h = (p * g);

        let r;

        consider b be Real such that

         A5: b > 0 and

         A6: for n be Nat holds |.(Rseq . n).| < b by A1, SEQ_2: 3, SEQ_2: 13;

        reconsider b as Real;



         A7: (b + ||.g.||) > ( 0 + 0 ) by A5, BHSP_1: 28, XREAL_1: 8;

        assume

         A8: r > 0 ;

        then

        consider m1 be Nat such that

         A9: for n be Nat st n >= m1 holds |.((Rseq . n) - p).| < (r / (b + ||.g.||)) by A3, A7, XREAL_1: 139;

        consider m2 be Nat such that

         A10: for n be Nat st n >= m2 holds ||.((seq . n) - g).|| < (r / (b + ||.g.||)) by A4, A7, A8, XREAL_1: 139;

        reconsider m = (m1 + m2) as Nat;

        take m;

        let n be Nat such that

         A11: n >= m;

        (m1 + m2) >= m1 by NAT_1: 12;

        then n >= m1 by A11, XXREAL_0: 2;

        then ||.g.|| >= 0 & |.((Rseq . n) - p).| <= (r / (b + ||.g.||)) by A9, BHSP_1: 28;

        then

         A12: ( ||.g.|| * |.((Rseq . n) - p).|) <= ( ||.g.|| * (r / (b + ||.g.||))) by XREAL_1: 64;



         A13: |.(Rseq . n).| >= 0 & ||.((seq . n) - g).|| >= 0 by BHSP_1: 28, COMPLEX1: 46;

        m >= m2 by NAT_1: 12;

        then n >= m2 by A11, XXREAL_0: 2;

        then

         A14: ||.((seq . n) - g).|| < (r / (b + ||.g.||)) by A10;

         |.(Rseq . n).| < b by A6;

        then ( |.(Rseq . n).| * ||.((seq . n) - g).||) < (b * (r / (b + ||.g.||))) by A14, A13, XREAL_1: 96;

        then (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Rseq . n) - p).|)) < ((b * (r / (b + ||.g.||))) + ( ||.g.|| * (r / (b + ||.g.||)))) by A12, XREAL_1: 8;

        then (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Rseq . n) - p).|)) < (((b * r) / (b + ||.g.||)) + ( ||.g.|| * (r / (b + ||.g.||)))) by XCMPLX_1: 74;

        then (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Rseq . n) - p).|)) < (((b * r) / (b + ||.g.||)) + (( ||.g.|| * r) / (b + ||.g.||))) by XCMPLX_1: 74;

        then (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Rseq . n) - p).|)) < (((b * r) + ( ||.g.|| * r)) / (b + ||.g.||)) by XCMPLX_1: 62;

        then (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Rseq . n) - p).|)) < (((b + ||.g.||) * r) / (b + ||.g.||));

        then

         A15: (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Rseq . n) - p).|)) < r by A7, XCMPLX_1: 89;

         ||.(((Rseq * seq) . n) - (p * g)).|| = ||.(((Rseq . n) * (seq . n)) - (p * g)).|| by Def7

        .= ||.((((Rseq . n) * (seq . n)) - (p * g)) + 09(X)).||

        .= ||.((((Rseq . n) * (seq . n)) - (p * g)) + (((Rseq . n) * g) - ((Rseq . n) * g))).|| by RLVECT_1: 15

        .= ||.(((Rseq . n) * (seq . n)) - ((p * g) - (((Rseq . n) * g) - ((Rseq . n) * g)))).|| by RLVECT_1: 29

        .= ||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * g) + ((p * g) - ((Rseq . n) * g)))).|| by RLVECT_1: 29

        .= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) - ((p * g) - ((Rseq . n) * g))).|| by RLVECT_1: 27

        .= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) + (((Rseq . n) * g) - (p * g))).|| by RLVECT_1: 33;

        then ||.(((Rseq * seq) . n) - (p * g)).|| <= ( ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * g)).|| + ||.(((Rseq . n) * g) - (p * g)).||) by BHSP_1: 30;

        then ||.(((Rseq * seq) . n) - (p * g)).|| <= ( ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) * g) - (p * g)).||) by RLVECT_1: 34;

        then ||.(((Rseq * seq) . n) - (p * g)).|| <= ( ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) - p) * g).||) by RLVECT_1: 35;

        then ||.(((Rseq * seq) . n) - (p * g)).|| <= (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ||.(((Rseq . n) - p) * g).||) by BHSP_1: 27;

        then ||.(((Rseq * seq) . n) - (p * g)).|| <= (( |.(Rseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Rseq . n) - p).|)) by BHSP_1: 27;

        hence ||.(((Rseq * seq) . n) - h).|| < r by A15, XXREAL_0: 2;

      end;

      hence thesis by BHSP_2: 9;

    end;

    theorem :: BHSP_4:49

    Rseq is bounded & seq is bounded implies (Rseq * seq) is bounded

    proof

      assume that

       A1: Rseq is bounded and

       A2: seq is bounded;

      consider M1 be Real such that

       A3: M1 > 0 and

       A4: for n be Nat holds |.(Rseq . n).| < M1 by A1, SEQ_2: 3;

      consider M2 such that

       A5: M2 > 0 and

       A6: for n holds ||.(seq . n).|| <= M2 by A2, BHSP_3:def 3;

      now

        reconsider M = (M1 * M2) as Real;

        take M;

        now

          let n;

           |.(Rseq . n).| >= 0 by COMPLEX1: 46;

          then

           A7: ( |.(Rseq . n).| * ||.(seq . n).||) <= ( |.(Rseq . n).| * M2) by A6, XREAL_1: 64;

           |.(Rseq . n).| <= M1 by A4;

          then

           A8: ( |.(Rseq . n).| * M2) <= (M1 * M2) by A5, XREAL_1: 64;

           ||.((Rseq * seq) . n).|| = ||.((Rseq . n) * (seq . n)).|| by Def7

          .= ( |.(Rseq . n).| * ||.(seq . n).||) by BHSP_1: 27;

          hence ||.((Rseq * seq) . n).|| <= M by A7, A8, XXREAL_0: 2;

        end;

        hence M > 0 & for n holds ||.((Rseq * seq) . n).|| <= M by A3, A5, XREAL_1: 129;

      end;

      hence thesis by BHSP_3:def 3;

    end;

    theorem :: BHSP_4:50

    Rseq is convergent & seq is convergent implies (Rseq * seq) is convergent & ( lim (Rseq * seq)) = (( lim Rseq) * ( lim seq))

    proof

      assume that

       A1: Rseq is convergent and

       A2: seq is convergent;

      consider b be Real such that

       A3: b > 0 and

       A4: for n be Nat holds |.(Rseq . n).| < b by A1, SEQ_2: 3, SEQ_2: 13;

      reconsider b as Real;



       A5: (b + ||.( lim seq).||) > ( 0 + 0 ) by A3, BHSP_1: 28, XREAL_1: 8;



       A6: ||.( lim seq).|| >= 0 by BHSP_1: 28;

       A7:

      now

        let r;

        assume r > 0 ;

        then

         A8: (r / (b + ||.( lim seq).||)) > 0 by A5, XREAL_1: 139;

        then

        consider m1 be Nat such that

         A9: for n be Nat st n >= m1 holds |.((Rseq . n) - ( lim Rseq)).| < (r / (b + ||.( lim seq).||)) by A1, SEQ_2:def 7;

        consider m2 be Nat such that

         A10: for n be Nat st n >= m2 holds ( dist ((seq . n),( lim seq))) < (r / (b + ||.( lim seq).||)) by A2, A8, BHSP_2:def 2;

        take m = (m1 + m2);

        let n be Nat such that

         A11: n >= m;

        (m1 + m2) >= m1 by NAT_1: 12;

        then n >= m1 by A11, XXREAL_0: 2;

        then |.((Rseq . n) - ( lim Rseq)).| <= (r / (b + ||.( lim seq).||)) by A9;

        then

         A12: ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|) <= ( ||.( lim seq).|| * (r / (b + ||.( lim seq).||))) by A6, XREAL_1: 64;



         A13: ||.((seq . n) - ( lim seq)).|| >= 0 by BHSP_1: 28;

        m >= m2 by NAT_1: 12;

        then n >= m2 by A11, XXREAL_0: 2;

        then ( dist ((seq . n),( lim seq))) < (r / (b + ||.( lim seq).||)) by A10;

        then

         A14: ||.((seq . n) - ( lim seq)).|| < (r / (b + ||.( lim seq).||)) by BHSP_1:def 5;

         |.(Rseq . n).| < b & |.(Rseq . n).| >= 0 by A4, COMPLEX1: 46;

        then ( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) < (b * (r / (b + ||.( lim seq).||))) by A14, A13, XREAL_1: 96;

        then (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|)) < ((b * (r / (b + ||.( lim seq).||))) + ( ||.( lim seq).|| * (r / (b + ||.( lim seq).||)))) by A12, XREAL_1: 8;

        then (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|)) < (((b * r) / (b + ||.( lim seq).||)) + ( ||.( lim seq).|| * (r / (b + ||.( lim seq).||)))) by XCMPLX_1: 74;

        then (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|)) < (((b * r) / (b + ||.( lim seq).||)) + (( ||.( lim seq).|| * r) / (b + ||.( lim seq).||))) by XCMPLX_1: 74;

        then (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|)) < (((b * r) + ( ||.( lim seq).|| * r)) / (b + ||.( lim seq).||)) by XCMPLX_1: 62;

        then (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|)) < (((b + ||.( lim seq).||) * r) / (b + ||.( lim seq).||));

        then

         A15: (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|)) < r by A5, XCMPLX_1: 89;

         ||.(((Rseq * seq) . n) - (( lim Rseq) * ( lim seq))).|| = ||.(((Rseq . n) * (seq . n)) - (( lim Rseq) * ( lim seq))).|| by Def7

        .= ||.((((Rseq . n) * (seq . n)) - (( lim Rseq) * ( lim seq))) + 09(X)).||

        .= ||.((((Rseq . n) * (seq . n)) - (( lim Rseq) * ( lim seq))) + (((Rseq . n) * ( lim seq)) - ((Rseq . n) * ( lim seq)))).|| by RLVECT_1: 15

        .= ||.(((Rseq . n) * (seq . n)) - ((( lim Rseq) * ( lim seq)) - (((Rseq . n) * ( lim seq)) - ((Rseq . n) * ( lim seq))))).|| by RLVECT_1: 29

        .= ||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * ( lim seq)) + ((( lim Rseq) * ( lim seq)) - ((Rseq . n) * ( lim seq))))).|| by RLVECT_1: 29

        .= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * ( lim seq))) - ((( lim Rseq) * ( lim seq)) - ((Rseq . n) * ( lim seq)))).|| by RLVECT_1: 27

        .= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * ( lim seq))) + (((Rseq . n) * ( lim seq)) - (( lim Rseq) * ( lim seq)))).|| by RLVECT_1: 33;

        then ||.(((Rseq * seq) . n) - (( lim Rseq) * ( lim seq))).|| <= ( ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * ( lim seq))).|| + ||.(((Rseq . n) * ( lim seq)) - (( lim Rseq) * ( lim seq))).||) by BHSP_1: 30;

        then ||.(((Rseq * seq) . n) - (( lim Rseq) * ( lim seq))).|| <= ( ||.((Rseq . n) * ((seq . n) - ( lim seq))).|| + ||.(((Rseq . n) * ( lim seq)) - (( lim Rseq) * ( lim seq))).||) by RLVECT_1: 34;

        then ||.(((Rseq * seq) . n) - (( lim Rseq) * ( lim seq))).|| <= ( ||.((Rseq . n) * ((seq . n) - ( lim seq))).|| + ||.(((Rseq . n) - ( lim Rseq)) * ( lim seq)).||) by RLVECT_1: 35;

        then ||.(((Rseq * seq) . n) - (( lim Rseq) * ( lim seq))).|| <= (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ||.(((Rseq . n) - ( lim Rseq)) * ( lim seq)).||) by BHSP_1: 27;

        then ||.(((Rseq * seq) . n) - (( lim Rseq) * ( lim seq))).|| <= (( |.(Rseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Rseq . n) - ( lim Rseq)).|)) by BHSP_1: 27;

        then ||.(((Rseq * seq) . n) - (( lim Rseq) * ( lim seq))).|| < r by A15, XXREAL_0: 2;

        hence ( dist (((Rseq * seq) . n),(( lim Rseq) * ( lim seq)))) < r by BHSP_1:def 5;

      end;

      (Rseq * seq) is convergent by A1, A2, Th48;

      hence thesis by A7, BHSP_2:def 2;

    end;

    definition

      let Rseq;

      :: BHSP_4:def8

      attr Rseq is Cauchy means for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds |.((Rseq . n) - (Rseq . m)).| < r;

    end

    theorem :: BHSP_4:51

    for X be RealHilbertSpace, seq be sequence of X holds seq is Cauchy & Rseq is Cauchy implies (Rseq * seq) is Cauchy

    proof

      let X be RealHilbertSpace, seq be sequence of X;

      assume that

       A1: seq is Cauchy and

       A2: Rseq is Cauchy;

      now

        let r be Real;

        assume

         A3: r > 0 ;

        consider k such that

         A4: for n, m st n >= k & m >= k holds |.((Rseq . n) - (Rseq . m)).| < r by A2, A3;

        reconsider k as Nat;

        take k;

        let n be Nat;

        thus n >= k implies |.((Rseq . n) - (Rseq . k)).| < r by A4;

      end;

      then

       A5: Rseq is convergent by SEQ_4: 41;

      (Rseq * seq) is convergent by A5, Th48, A1, BHSP_3:def 4;

      hence thesis;

    end;

    theorem :: BHSP_4:52



     Th52: for n holds (( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) = ((( Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * ( Partial_Sums seq)) . (n + 1)))

    proof

      defpred P[ Nat] means (( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . $1) = ((( Partial_Sums (Rseq * seq)) . ($1 + 1)) - ((Rseq * ( Partial_Sums seq)) . ($1 + 1)));



       A1: (( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . 0 ) = (((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq)) . 0 ) by Def1

      .= (((Rseq - (Rseq ^\ 1)) . 0 ) * (( Partial_Sums seq) . 0 )) by Def7

      .= (((Rseq + ( - (Rseq ^\ 1))) . 0 ) * (seq . 0 )) by Def1

      .= (((Rseq . 0 ) + (( - (Rseq ^\ 1)) . 0 )) * (seq . 0 )) by SEQ_1: 7

      .= (((Rseq . 0 ) + ( - ((Rseq ^\ 1) . 0 ))) * (seq . 0 )) by SEQ_1: 10

      .= (((Rseq . 0 ) - ((Rseq ^\ 1) . 0 )) * (seq . 0 ))

      .= (((Rseq . 0 ) - (Rseq . ( 0 + 1))) * (seq . 0 )) by NAT_1:def 3

      .= (((Rseq . 0 ) * (seq . 0 )) - ((Rseq . 1) * (seq . 0 ))) by RLVECT_1: 35;



       A2: ((Rseq * ( Partial_Sums seq)) . ( 0 + 1)) = ((Rseq . ( 0 + 1)) * (( Partial_Sums seq) . ( 0 + 1))) by Def7

      .= ((Rseq . ( 0 + 1)) * ((( Partial_Sums seq) . 0 ) + (seq . ( 0 + 1)))) by Def1

      .= ((Rseq . 1) * ((seq . 0 ) + (seq . 1))) by Def1

      .= (((Rseq . 1) * (seq . 0 )) + ((Rseq . 1) * (seq . 1))) by RLVECT_1:def 5;

       A3:

      now

        let n;

        assume P[n];

        then ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((Rseq * ( Partial_Sums seq)) . (n + 1))) = ((( Partial_Sums (Rseq * seq)) . (n + 1)) - (((Rseq * ( Partial_Sums seq)) . (n + 1)) - ((Rseq * ( Partial_Sums seq)) . (n + 1)))) by RLVECT_1: 29;

        then

         A4: ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((Rseq * ( Partial_Sums seq)) . (n + 1))) = ((( Partial_Sums (Rseq * seq)) . (n + 1)) - 09(X)) by RLVECT_1: 15;

        (( Partial_Sums (Rseq * seq)) . ((n + 1) + 1)) = ((( Partial_Sums (Rseq * seq)) . (n + 1)) + ((Rseq * seq) . ((n + 1) + 1))) by Def1

        .= (((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((Rseq * ( Partial_Sums seq)) . (n + 1))) + ((Rseq * seq) . ((n + 1) + 1))) by A4

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((Rseq * ( Partial_Sums seq)) . (n + 1)) + ((Rseq * seq) . ((n + 1) + 1)))) by RLVECT_1:def 3

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((Rseq . (n + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Rseq * seq) . ((n + 1) + 1)))) by Def7

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) + (Rseq . ((n + 1) + 1))) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by Def7

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by RLVECT_1:def 6

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1))) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by NAT_1:def 3

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) + ( - ((Rseq ^\ 1) . (n + 1)))) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))))

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) + (( - (Rseq ^\ 1)) . (n + 1))) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by SEQ_1: 10

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Rseq - (Rseq ^\ 1)) . (n + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by SEQ_1: 7

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((((Rseq - (Rseq ^\ 1)) . (n + 1)) * (( Partial_Sums seq) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))))) by RLVECT_1:def 3

        .= (((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((Rseq - (Rseq ^\ 1)) . (n + 1)) * (( Partial_Sums seq) . (n + 1)))) + (((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by RLVECT_1:def 3

        .= (((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq)) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by Def7

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + (((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by Def1

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * ((( Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1))))) by RLVECT_1:def 5

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * (( Partial_Sums seq) . ((n + 1) + 1)))) by Def1

        .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + ((Rseq * ( Partial_Sums seq)) . ((n + 1) + 1))) by Def7;

        then ((( Partial_Sums (Rseq * seq)) . ((n + 1) + 1)) - ((Rseq * ( Partial_Sums seq)) . ((n + 1) + 1))) = ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + (((Rseq * ( Partial_Sums seq)) . ((n + 1) + 1)) - ((Rseq * ( Partial_Sums seq)) . ((n + 1) + 1)))) by RLVECT_1:def 3;

        then ((( Partial_Sums (Rseq * seq)) . ((n + 1) + 1)) - ((Rseq * ( Partial_Sums seq)) . ((n + 1) + 1))) = ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + 09(X)) by RLVECT_1: 15;

        hence P[(n + 1)];

      end;

      (( Partial_Sums (Rseq * seq)) . ( 0 + 1)) = ((( Partial_Sums (Rseq * seq)) . 0 ) + ((Rseq * seq) . ( 0 + 1))) by Def1

      .= (((Rseq * seq) . 0 ) + ((Rseq * seq) . 1)) by Def1

      .= (((Rseq . 0 ) * (seq . 0 )) + ((Rseq * seq) . 1)) by Def7

      .= (((Rseq . 0 ) * (seq . 0 )) + ((Rseq . 1) * (seq . 1))) by Def7;



      then (( Partial_Sums (Rseq * seq)) . ( 0 + 1)) = ((((Rseq . 0 ) * (seq . 0 )) + 09(X)) + ((Rseq . 1) * (seq . 1)))

      .= ((((Rseq . 0 ) * (seq . 0 )) + (((Rseq . 1) * (seq . 0 )) - ((Rseq . 1) * (seq . 0 )))) + ((Rseq . 1) * (seq . 1))) by RLVECT_1: 15

      .= (((((Rseq . 0 ) * (seq . 0 )) + ( - ((Rseq . 1) * (seq . 0 )))) + ((Rseq . 1) * (seq . 0 ))) + ((Rseq . 1) * (seq . 1))) by RLVECT_1:def 3

      .= ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . 0 ) + ((Rseq * ( Partial_Sums seq)) . ( 0 + 1))) by A1, A2, RLVECT_1:def 3;

      then ((( Partial_Sums (Rseq * seq)) . ( 0 + 1)) - ((Rseq * ( Partial_Sums seq)) . ( 0 + 1))) = ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . 0 ) + (((Rseq * ( Partial_Sums seq)) . ( 0 + 1)) - ((Rseq * ( Partial_Sums seq)) . ( 0 + 1)))) by RLVECT_1:def 3;

      then ((( Partial_Sums (Rseq * seq)) . ( 0 + 1)) - ((Rseq * ( Partial_Sums seq)) . ( 0 + 1))) = ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . 0 ) + 09(X)) by RLVECT_1: 15;

      then

       A5: P[ 0 ];

      thus for n holds P[n] from NAT_1:sch 2( A5, A3);

    end;

    theorem :: BHSP_4:53



     Th53: for n holds (( Partial_Sums (Rseq * seq)) . (n + 1)) = (((Rseq * ( Partial_Sums seq)) . (n + 1)) - (( Partial_Sums (((Rseq ^\ 1) - Rseq) * ( Partial_Sums seq))) . n))

    proof

      let n;

      ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((Rseq * ( Partial_Sums seq)) . (n + 1))) = (((( Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * ( Partial_Sums seq)) . (n + 1))) + ((Rseq * ( Partial_Sums seq)) . (n + 1))) by Th52;

      then ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((Rseq * ( Partial_Sums seq)) . (n + 1))) = ((( Partial_Sums (Rseq * seq)) . (n + 1)) - (((Rseq * ( Partial_Sums seq)) . (n + 1)) - ((Rseq * ( Partial_Sums seq)) . (n + 1)))) by RLVECT_1: 29;

      then ((( Partial_Sums ((Rseq - (Rseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((Rseq * ( Partial_Sums seq)) . (n + 1))) = ((( Partial_Sums (Rseq * seq)) . (n + 1)) - 09(X)) by RLVECT_1: 15;

      then (( Partial_Sums (Rseq * seq)) . (n + 1)) = (((Rseq * ( Partial_Sums seq)) . (n + 1)) + (( Partial_Sums (((( - 1) (#) (Rseq ^\ 1)) - ( - Rseq)) * ( Partial_Sums seq))) . n));

      then (( Partial_Sums (Rseq * seq)) . (n + 1)) = (((Rseq * ( Partial_Sums seq)) . (n + 1)) + (( Partial_Sums ((( - 1) (#) ((Rseq ^\ 1) - Rseq)) * ( Partial_Sums seq))) . n)) by SEQ_1: 24;

      then (( Partial_Sums (Rseq * seq)) . (n + 1)) = (((Rseq * ( Partial_Sums seq)) . (n + 1)) + (( Partial_Sums (( - 1) * (((Rseq ^\ 1) - Rseq) * ( Partial_Sums seq)))) . n)) by Th46;

      then (( Partial_Sums (Rseq * seq)) . (n + 1)) = (((Rseq * ( Partial_Sums seq)) . (n + 1)) + ((( - 1) * ( Partial_Sums (((Rseq ^\ 1) - Rseq) * ( Partial_Sums seq)))) . n)) by Th3;

      then (( Partial_Sums (Rseq * seq)) . (n + 1)) = (((Rseq * ( Partial_Sums seq)) . (n + 1)) + (( - 1) * (( Partial_Sums (((Rseq ^\ 1) - Rseq) * ( Partial_Sums seq))) . n))) by NORMSP_1:def 5;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: BHSP_4:54

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