clvect_3.miz

    begin

    reserve X for ComplexUnitarySpace;

    reserve g for Point of X;

    reserve seq,seq1,seq2 for sequence of X;

    reserve Rseq for Real_Sequence;

    reserve Cseq,Cseq1,Cseq2 for Complex_Sequence;

    reserve z,z1,z2 for Complex;

    reserve r for Real;

    reserve k,n,m for Nat;

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

    theorem :: CLVECT_3:1



     Th1: (( Partial_Sums seq1) + ( Partial_Sums seq2)) = ( Partial_Sums (seq1 + seq2))

    proof

      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 BHSP_4:def 1

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

        .= ((((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 BHSP_4:def 1

      .= ((seq1 . 0 ) + (seq2 . 0 )) by BHSP_4:def 1

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

      hence thesis by A1, BHSP_4:def 1;

    end;

    theorem :: CLVECT_3:2



     Th2: (( Partial_Sums seq1) - ( Partial_Sums seq2)) = ( Partial_Sums (seq1 - seq2))

    proof

      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 BHSP_4:def 1

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

        .= ((((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 BHSP_4:def 1

      .= ((seq1 . 0 ) - (seq2 . 0 )) by BHSP_4:def 1

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

      hence thesis by A1, BHSP_4:def 1;

    end;

    theorem :: CLVECT_3:3



     Th3: ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq))

    proof

      set PSseq = ( Partial_Sums seq);

       A1:

      now

        let n;



        thus ((z * PSseq) . (n + 1)) = (z * (PSseq . (n + 1))) by CLVECT_1:def 14

        .= (z * ((PSseq . n) + (seq . (n + 1)))) by BHSP_4:def 1

        .= ((z * (PSseq . n)) + (z * (seq . (n + 1)))) by CLVECT_1:def 2

        .= (((z * PSseq) . n) + (z * (seq . (n + 1)))) by CLVECT_1:def 14

        .= (((z * PSseq) . n) + ((z * seq) . (n + 1))) by CLVECT_1:def 14;

      end;

      ((z * PSseq) . 0 ) = (z * (PSseq . 0 )) by CLVECT_1:def 14

      .= (z * (seq . 0 )) by BHSP_4:def 1

      .= ((z * seq) . 0 ) by CLVECT_1:def 14;

      hence thesis by A1, BHSP_4:def 1;

    end;

    theorem :: CLVECT_3:4

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

    proof

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

      then ( Partial_Sums ( - seq)) = (( - 1r ) * ( Partial_Sums seq)) by CSSPACE: 70;

      hence thesis by CSSPACE: 70;

    end;

    theorem :: CLVECT_3:5

    ((z1 * ( Partial_Sums seq1)) + (z2 * ( Partial_Sums seq2))) = ( Partial_Sums ((z1 * seq1) + (z2 * seq2)))

    proof



      thus ((z1 * ( Partial_Sums seq1)) + (z2 * ( Partial_Sums seq2))) = (( Partial_Sums (z1 * seq1)) + (z2 * ( Partial_Sums seq2))) by Th3

      .= (( Partial_Sums (z1 * seq1)) + ( Partial_Sums (z2 * seq2))) by Th3

      .= ( Partial_Sums ((z1 * seq1) + (z2 * seq2))) by Th1;

    end;

    definition

      let X, seq;

      :: CLVECT_3:def1

      attr seq is summable means

      : Def1: ( Partial_Sums seq) is convergent;

      :: CLVECT_3:def2

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

      correctness ;

    end

    theorem :: CLVECT_3: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 CLVECT_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, CLVECT_2: 13;

    end;

    theorem :: CLVECT_3: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 CLVECT_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, CLVECT_2: 14;

    end;

    theorem :: CLVECT_3:8

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

    proof

      assume seq is summable;

      then

       A1: ( Partial_Sums seq) is convergent;

      then (z * ( Partial_Sums seq)) is convergent by CLVECT_2: 5;

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

      hence (z * seq) is summable;



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

      .= (z * ( Sum seq)) by A1, CLVECT_2: 15;

    end;

    theorem :: CLVECT_3: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 BHSP_4:def 1

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

      now

        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) by RLVECT_1: 4;

      end;

      then ((seq ^\ 1) + (PSseq - PSseq)) = (seq ^\ 1) by FUNCT_2: 63;

      then

       A2: (seq ^\ 1) = ((PSseq ^\ 1) - PSseq) by A1, CSSPACE: 76;

      assume seq is summable;

      then

       A3: PSseq is convergent;

      then

       A4: (PSseq ^\ 1) is convergent by CLVECT_2: 90;

      then

       A5: (seq ^\ 1) is convergent by A3, A2, CLVECT_2: 4;

      hence seq is convergent by CLVECT_2: 91;

      ( lim (PSseq ^\ 1)) = ( lim PSseq) by A3, CLVECT_2: 90;



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

      .= 09(X) by RLVECT_1: 15;

      hence thesis by A2, A5, CLVECT_2: 84, CLVECT_2: 91;

    end;

    theorem :: CLVECT_3:10



     Th10: for X be ComplexHilbertSpace, 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 CLVECT_2: 65, CLVECT_2: 58, CLVECT_2:def 11;

    theorem :: CLVECT_3:11

    seq is summable implies ( Partial_Sums seq) is bounded by CLVECT_2: 80;

    theorem :: CLVECT_3:12



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

    proof

      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 BHSP_4:def 1

        .= (((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 BHSP_4:def 1

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

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

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

      .= (seq . ( 0 + 1)) by RLVECT_1: 4

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

      hence thesis by A2, BHSP_4:def 1;

    end;

    theorem :: CLVECT_3: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 ( Partial_Sums (seq ^\ k)) is convergent;

        then

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

        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, CLVECT_2: 1;

        then (seq ^\ (k + 1)) = ((seq ^\ k) ^\ 1) & ( Partial_Sums ((seq ^\ k) ^\ 1)) is convergent by A2, CLVECT_2: 4, NAT_1: 48;

        hence thesis by Def1;

      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 :: CLVECT_3: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 BHSP_4:def 1

      .= (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 BHSP_4:def 1

        .= (((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 BHSP_4:def 1

        .= (( 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 BHSP_4:def 1

      .= ((( 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 NAT_1: 48;

      seq1 is convergent by CLVECT_2: 1;

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

      then ( Partial_Sums seq) is convergent by CLVECT_2: 91;

      hence thesis;

    end;

    definition

      let X, seq, n;

      :: CLVECT_3:def3

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

      correctness ;

    end

    theorem :: CLVECT_3:15

    ( Sum (seq, 0 )) = (seq . 0 ) by BHSP_4:def 1;

    theorem :: CLVECT_3:16



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

    proof

      (( Partial_Sums seq) . 1) = ((( Partial_Sums seq) . 0 ) + (seq . ( 0 + 1))) by BHSP_4:def 1

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

      hence thesis;

    end;

    theorem :: CLVECT_3: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 BHSP_4:def 1;

    end;

    theorem :: CLVECT_3:18

    ( Sum (seq,(n + 1))) = (( Sum (seq,n)) + (seq . (n + 1))) by BHSP_4:def 1;

    theorem :: CLVECT_3: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 BHSP_4:def 1

      .= ((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)) by RLVECT_1: 4;

    end;

    theorem :: CLVECT_3: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;

      :: CLVECT_3:def4

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

      correctness ;

    end

    theorem :: CLVECT_3: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 BHSP_4:def 1

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

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

      hence thesis by RLVECT_1: 4;

    end;

    theorem :: CLVECT_3:22

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

    theorem :: CLVECT_3:23



     Th23: for X be ComplexHilbertSpace, 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 ComplexHilbertSpace, 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 :: CLVECT_3:24

    for X be ComplexHilbertSpace, 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 ComplexHilbertSpace, 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 Cseq, n;

      :: CLVECT_3:def5

      func Sum (Cseq,n) -> Complex equals (( Partial_Sums Cseq) . n);

      correctness ;

    end

    definition

      let Cseq, n, m;

      :: CLVECT_3:def6

      func Sum (Cseq,n,m) -> Complex equals (( Sum (Cseq,n)) - ( Sum (Cseq,m)));

      correctness ;

    end

    definition

      let X, seq;

      :: CLVECT_3:def7

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

    end

    theorem :: CLVECT_3:25

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

    proof



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

      proof

        let n;

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

        hence ( ||.(seq1 + seq2).|| . n) >= 0 by CSSPACE: 44;

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

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

        then ( ||.(seq1 + seq2).|| . n) <= ( ||.(seq1 . n).|| + ||.(seq2 . n).||) by CSSPACE: 46;

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

        then ( ||.(seq1 + seq2).|| . n) <= (( ||.seq1.|| . n) + ( ||.seq2.|| . n)) by CLVECT_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 :: CLVECT_3:26

    seq is absolutely_summable implies (z * seq) is absolutely_summable

    proof



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

      proof

        let n;

        ( ||.(z * seq).|| . n) = ||.((z * seq) . n).|| by CLVECT_2:def 3;

        hence ( ||.(z * seq).|| . n) >= 0 by CSSPACE: 44;

        ( ||.(z * seq).|| . n) = ||.((z * seq) . n).|| by CLVECT_2:def 3

        .= ||.(z * (seq . n)).|| by CLVECT_1:def 14

        .= ( |.z.| * ||.(seq . n).||) by CSSPACE: 43

        .= ( |.z.| * ( ||.seq.|| . n)) by CLVECT_2:def 3

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

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

      end;

      assume seq is absolutely_summable;

      then ||.seq.|| is summable;

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

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

      hence thesis;

    end;

    theorem :: CLVECT_3:27

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

    proof



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

      proof

        let n;

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

        hence thesis by CSSPACE: 44;

      end;

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

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

      hence thesis;

    end;

    theorem :: CLVECT_3:28

    (for n 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 holds (seq . n) <> 09(X) & (Rseq . n) = ( ||.(seq . (n + 1)).|| / ||.(seq . n).||) and

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

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

      proof

        let n;

        (seq . n) <> 09(X) by A1;

        then

         A3: ||.(seq . n).|| <> 0 by CSSPACE: 42;

         ||.(seq . n).|| >= 0 by CSSPACE: 44;

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

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

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

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

      end;

      then ||.seq.|| is summable by A2, SERIES_1: 26;

      hence thesis;

    end;

    theorem :: CLVECT_3: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;

      now

        per cases ;

          suppose not seq is convergent;

          hence thesis;

        end;

          suppose

           A3: seq is convergent;

          now

            assume ( lim seq) = 09(X);

            then

            consider k such that

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

            now

              let n;

              assume

               A5: n >= (m + k);

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

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

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

              then

               A6: ||.(seq . n).|| < r by RLVECT_1: 13;

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

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

              hence contradiction by A2, A6;

            end;

            hence contradiction;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_3: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).||;

          (seq . (m + k)) <> 09(X) by A1;

          then

           A6: ||.(seq . (m + k)).|| <> 0 by CSSPACE: 42;

          ( ||.(seq . ((m + k) + 1)).|| / ||.(seq . (m + k)).||) >= 1 & ||.(seq . (m + k)).|| >= 0 by A2, CSSPACE: 44, 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;

      (seq . m) <> 09(X) by A1;

      then ||.(seq . m).|| <> 0 by CSSPACE: 42;

      then ||.(seq . m).|| > 0 by CSSPACE: 44;

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

      hence thesis by Th9;

    end;

    theorem :: CLVECT_3: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 such that

       A5: for n 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 :: CLVECT_3: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 holds ( ||.seq.|| . n) >= 0 & (Rseq . n) = (n -root ( ||.seq.|| . n))

      proof

        let n;

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

        hence ( ||.seq.|| . n) >= 0 by CSSPACE: 44;

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

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

      end;

      then ||.seq.|| is summable by A2, SERIES_1: 28;

      hence thesis;

    end;

    theorem :: CLVECT_3: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 CLVECT_2:def 3;

        then ||.(seq . n).|| >= 0 & ((n -root ||.(seq . n).||) |^ n) >= 1 by A2, A5, CSSPACE: 44, 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 :: CLVECT_3: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 such that

       A4: for n 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 CLVECT_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 CSSPACE: 44, 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 :: CLVECT_3:35



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

    proof

      now

        let n;

         ||.(seq . (n + 1)).|| >= 0 by CSSPACE: 44;

        then ( ||.seq.|| . (n + 1)) >= 0 by CLVECT_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 :: CLVECT_3:36

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

    proof

      let n;

       ||.(seq . 0 ).|| >= 0 by CSSPACE: 44;

      then ( ||.seq.|| . 0 ) >= 0 by CLVECT_2:def 3;

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

      hence thesis by Th35, SEQM_3: 11;

    end;

    theorem :: CLVECT_3: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;

        (( Partial_Sums seq) . (n + 1)) = ((( Partial_Sums seq) . n) + (seq . (n + 1))) by BHSP_4:def 1;

        then

         A2: ||.(( Partial_Sums seq) . (n + 1)).|| <= ( ||.(( Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).||) by CSSPACE: 46;

        assume P[n];

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

        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 CLVECT_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 CLVECT_2:def 3;

      then

       A3: P[ 0 ] by BHSP_4:def 1;

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

    end;

    theorem :: CLVECT_3:38

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

    proof

      let n;

       ||.(( Partial_Sums seq) . n).|| <= (( Partial_Sums ||.seq.||) . n) by Th37;

      hence thesis by SERIES_1:def 5;

    end;

    theorem :: CLVECT_3: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 CSSPACE: 44;



           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 CLVECT_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 BHSP_4:def 1

          .= ||.(((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 CSSPACE: 46;

          then

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

          (PSseq9 . (m + k)) >= (PSseq9 . m) by A2, SEQM_3: 5;

          then

           A7: ((PSseq9 . (m + k)) - (PSseq9 . m)) >= 0 by 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 CSSPACE: 42;

        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: |.((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 CLVECT_2:def 3

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

           ||.((PSseq . (n + (k + 1))) - (PSseq . n)).|| = ||.(((seq . ((n + k) + 1)) + (PSseq . (n + k))) - (PSseq . n)).|| by BHSP_4:def 1

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

          then

           A13: ||.((PSseq . (n + (k + 1))) - (PSseq . n)).|| <= ( ||.(seq . ((n + k) + 1)).|| + ||.((PSseq . (n + k)) - (PSseq . n)).||) by CSSPACE: 46;

          (PSseq9 . (n + k)) >= (PSseq9 . n) by A10, SEQM_3: 5;

          then

           A14: ((PSseq9 . (n + k)) - (PSseq9 . n)) >= 0 by XREAL_1: 48;

          assume P[k];

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

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

          then

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

           ||.(seq . ((n + k) + 1)).|| >= 0 by CSSPACE: 44;

          hence P[(k + 1)] by A14, A15, A12, 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 CSSPACE: 42;

        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 :: CLVECT_3:40



     Th40: for n, m holds ||.(( Sum (seq,m)) - ( Sum (seq,n))).|| <= |.(( Sum ( ||.seq.||,m)) - ( Sum ( ||.seq.||,n))).|

    proof

      let n, m;

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

      then ||.(( Sum (seq,m)) - ( Sum (seq,n))).|| <= |.(( Sum ( ||.seq.||,m)) - (( Partial_Sums ||.seq.||) . n)).| by SERIES_1:def 5;

      hence thesis by SERIES_1:def 5;

    end;

    theorem :: CLVECT_3:41

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

    proof

      let n, m;

       ||.(( Sum (seq,m)) - ( Sum (seq,n))).|| <= |.(( Sum ( ||.seq.||,m)) - ( Sum ( ||.seq.||,n))).| by Th40;

      hence thesis by SERIES_1:def 6;

    end;

    theorem :: CLVECT_3:42

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

    proof

      let X be ComplexHilbertSpace, seq be sequence of X such that

       A1: seq is absolutely_summable;



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

      now

        let r;

        assume r > 0 ;

        then (r / 2) > 0 ;

        then

        consider k such that

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

        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, Cseq;

      :: CLVECT_3:def8

      func Cseq * seq -> sequence of X means

      : Def8: for n holds (it . n) = ((Cseq . n) * (seq . n));

      existence

      proof

        deffunc F( Nat) = ((Cseq . $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 be Nat;

        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) = ((Cseq . n) * (seq . n)) and

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

        now

          let n be Element of NAT ;

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

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

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: CLVECT_3:43

    (Cseq * (seq1 + seq2)) = ((Cseq * seq1) + (Cseq * seq2))

    proof

      now

        let n be Element of NAT ;



        thus ((Cseq * (seq1 + seq2)) . n) = ((Cseq . n) * ((seq1 + seq2) . n)) by Def8

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

        .= (((Cseq . n) * (seq1 . n)) + ((Cseq . n) * (seq2 . n))) by CLVECT_1:def 2

        .= (((Cseq * seq1) . n) + ((Cseq . n) * (seq2 . n))) by Def8

        .= (((Cseq * seq1) . n) + ((Cseq * seq2) . n)) by Def8

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_3:44

    ((Cseq1 + Cseq2) * seq) = ((Cseq1 * seq) + (Cseq2 * seq))

    proof

      now

        let n be Element of NAT ;



        thus (((Cseq1 + Cseq2) * seq) . n) = (((Cseq1 + Cseq2) . n) * (seq . n)) by Def8

        .= (((Cseq1 . n) + (Cseq2 . n)) * (seq . n)) by VALUED_1: 1

        .= (((Cseq1 . n) * (seq . n)) + ((Cseq2 . n) * (seq . n))) by CLVECT_1:def 3

        .= (((Cseq1 * seq) . n) + ((Cseq2 . n) * (seq . n))) by Def8

        .= (((Cseq1 * seq) . n) + ((Cseq2 * seq) . n)) by Def8

        .= (((Cseq1 * seq) + (Cseq2 * seq)) . n) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_3:45

    ((Cseq1 (#) Cseq2) * seq) = (Cseq1 * (Cseq2 * seq))

    proof

      now

        let n be Element of NAT ;



        thus (((Cseq1 (#) Cseq2) * seq) . n) = (((Cseq1 (#) Cseq2) . n) * (seq . n)) by Def8

        .= (((Cseq1 . n) * (Cseq2 . n)) * (seq . n)) by VALUED_1: 5

        .= ((Cseq1 . n) * ((Cseq2 . n) * (seq . n))) by CLVECT_1:def 4

        .= ((Cseq1 . n) * ((Cseq2 * seq) . n)) by Def8

        .= ((Cseq1 * (Cseq2 * seq)) . n) by Def8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_3:46



     Th46: ((z (#) Cseq) * seq) = (z * (Cseq * seq))

    proof

      now

        let n be Element of NAT ;



        thus (((z (#) Cseq) * seq) . n) = (((z (#) Cseq) . n) * (seq . n)) by Def8

        .= ((z * (Cseq . n)) * (seq . n)) by VALUED_1: 6

        .= (z * ((Cseq . n) * (seq . n))) by CLVECT_1:def 4

        .= (z * ((Cseq * seq) . n)) by Def8

        .= ((z * (Cseq * seq)) . n) by CLVECT_1:def 14;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_3:47

    (Cseq * ( - seq)) = (( - Cseq) * seq)

    proof

      now

        let n be Element of NAT ;



        thus ((Cseq * ( - seq)) . n) = ((Cseq . n) * (( - seq) . n)) by Def8

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

        .= (( - (Cseq . n)) * (seq . n)) by CLVECT_1: 6

        .= ((( - Cseq) . n) * (seq . n)) by VALUED_1: 8

        .= ((( - Cseq) * seq) . n) by Def8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_3:48



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

    proof

      assume that

       A1: Cseq is convergent and

       A2: seq is convergent;

      consider p be Complex such that

       A3: for r be Real st r > 0 holds ex m st for n st n >= m holds |.((Cseq . n) - p).| < r by A1, COMSEQ_2:def 5;

      consider g such that

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

      now

        take h = (p * g);

        let r;

        Cseq is bounded by A1;

        then

        consider b be Real such that

         A5: b > 0 and

         A6: for n holds |.(Cseq . n).| < b by COMSEQ_2: 8;



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

        assume

         A8: r > 0 ;

        then

        consider m1 be Nat such that

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

        consider m2 be Nat such that

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

        take m = (m1 + m2);

        let n such that

         A11: n >= m;

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

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

        then ||.g.|| >= 0 & |.((Cseq . n) - p).| <= (r / (b + ||.g.||)) by A9, CSSPACE: 44;

        then

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



         A13: |.(Cseq . n).| >= 0 & ||.((seq . n) - g).|| >= 0 by COMPLEX1: 46, CSSPACE: 44;

        m >= m2 by NAT_1: 12;

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

        then

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

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

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

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

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

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

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

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

        then

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

         ||.(((Cseq * seq) . n) - (p * g)).|| = ||.(((Cseq . n) * (seq . n)) - (p * g)).|| by Def8

        .= ||.((((Cseq . n) * (seq . n)) - (p * g)) + 09(X)).|| by RLVECT_1: 4

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

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

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

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

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

        then ||.(((Cseq * seq) . n) - (p * g)).|| <= ( ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * g)).|| + ||.(((Cseq . n) * g) - (p * g)).||) by CSSPACE: 46;

        then ||.(((Cseq * seq) . n) - (p * g)).|| <= ( ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) * g) - (p * g)).||) by CLVECT_1: 9;

        then ||.(((Cseq * seq) . n) - (p * g)).|| <= ( ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) - p) * g).||) by CLVECT_1: 10;

        then ||.(((Cseq * seq) . n) - (p * g)).|| <= (( |.(Cseq . n).| * ||.((seq . n) - g).||) + ||.(((Cseq . n) - p) * g).||) by CSSPACE: 43;

        then ||.(((Cseq * seq) . n) - (p * g)).|| <= (( |.(Cseq . n).| * ||.((seq . n) - g).||) + ( ||.g.|| * |.((Cseq . n) - p).|)) by CSSPACE: 43;

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

      end;

      hence thesis by CLVECT_2: 9;

    end;

    theorem :: CLVECT_3:49

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

    proof

      assume that

       A1: Cseq is bounded and

       A2: seq is bounded;

      consider M1 be Real such that

       A3: M1 > 0 and

       A4: for n holds |.(Cseq . n).| < M1 by A1, COMSEQ_2: 8;

      consider M2 be Real such that

       A5: M2 > 0 and

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

      now

        set M = (M1 * M2);

        take M;

        now

          let n;

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

          then

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

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

          then

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

           ||.((Cseq * seq) . n).|| = ||.((Cseq . n) * (seq . n)).|| by Def8

          .= ( |.(Cseq . n).| * ||.(seq . n).||) by CSSPACE: 43;

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

        end;

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

      end;

      hence thesis by CLVECT_2:def 10;

    end;

    theorem :: CLVECT_3:50

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

    proof

      assume that

       A1: Cseq is convergent and

       A2: seq is convergent;

      Cseq is bounded by A1;

      then

      consider b be Real such that

       A3: b > 0 and

       A4: for n holds |.(Cseq . n).| < b by COMSEQ_2: 8;



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



       A6: ||.( lim seq).|| >= 0 by CSSPACE: 44;

       A7:

      now

        let r;

        assume r > 0 ;

        then

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

        then

        consider m1 be Nat such that

         A9: for n st n >= m1 holds |.((Cseq . n) - ( lim Cseq)).| < (r / (b + ||.( lim seq).||)) by A1, COMSEQ_2:def 6;

        consider m2 be Nat such that

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

        take m = (m1 + m2);

        let n such that

         A11: n >= m;

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

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

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

        then

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



         A13: ||.((seq . n) - ( lim seq)).|| >= 0 by CSSPACE: 44;

        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 CSSPACE:def 16;

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

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

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

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

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

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

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

        then

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

         ||.(((Cseq * seq) . n) - (( lim Cseq) * ( lim seq))).|| = ||.(((Cseq . n) * (seq . n)) - (( lim Cseq) * ( lim seq))).|| by Def8

        .= ||.((((Cseq . n) * (seq . n)) - (( lim Cseq) * ( lim seq))) + 09(X)).|| by RLVECT_1: 4

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

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

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

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

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

        then ||.(((Cseq * seq) . n) - (( lim Cseq) * ( lim seq))).|| <= ( ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * ( lim seq))).|| + ||.(((Cseq . n) * ( lim seq)) - (( lim Cseq) * ( lim seq))).||) by CSSPACE: 46;

        then ||.(((Cseq * seq) . n) - (( lim Cseq) * ( lim seq))).|| <= ( ||.((Cseq . n) * ((seq . n) - ( lim seq))).|| + ||.(((Cseq . n) * ( lim seq)) - (( lim Cseq) * ( lim seq))).||) by CLVECT_1: 9;

        then ||.(((Cseq * seq) . n) - (( lim Cseq) * ( lim seq))).|| <= ( ||.((Cseq . n) * ((seq . n) - ( lim seq))).|| + ||.(((Cseq . n) - ( lim Cseq)) * ( lim seq)).||) by CLVECT_1: 10;

        then ||.(((Cseq * seq) . n) - (( lim Cseq) * ( lim seq))).|| <= (( |.(Cseq . n).| * ||.((seq . n) - ( lim seq)).||) + ||.(((Cseq . n) - ( lim Cseq)) * ( lim seq)).||) by CSSPACE: 43;

        then ||.(((Cseq * seq) . n) - (( lim Cseq) * ( lim seq))).|| <= (( |.(Cseq . n).| * ||.((seq . n) - ( lim seq)).||) + ( ||.( lim seq).|| * |.((Cseq . n) - ( lim Cseq)).|)) by CSSPACE: 43;

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

        hence ( dist (((Cseq * seq) . n),(( lim Cseq) * ( lim seq)))) < r by CSSPACE:def 16;

      end;

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

      hence thesis by A7, CLVECT_2:def 2;

    end;

    definition

      let Cseq;

      :: CLVECT_3:def9

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

    end

    theorem :: CLVECT_3:51

    for X be ComplexHilbertSpace, seq be sequence of X holds seq is Cauchy & Cseq is Cauchy implies (Cseq * seq) is Cauchy

    proof

      let X be ComplexHilbertSpace, seq be sequence of X;

      assume that

       A1: seq is Cauchy and

       A2: Cseq is Cauchy;

      now

        let r be Real;

        assume r > 0 ;

        then

        consider k such that

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

        take k;

        thus for n st n >= k holds |.((Cseq . n) - (Cseq . k)).| < r by A3;

      end;

      then

       A4: Cseq is convergent by COMSEQ_3: 46;

      seq is convergent by A1, CLVECT_2:def 11;

      hence thesis by A4, Th48, CLVECT_2: 65;

    end;

    theorem :: CLVECT_3:52



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

    proof

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



       A1: (( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . 0 ) = (((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq)) . 0 ) by BHSP_4:def 1

      .= (((Cseq - (Cseq ^\ 1)) . 0 ) * (( Partial_Sums seq) . 0 )) by Def8

      .= (((Cseq + ( - (Cseq ^\ 1))) . 0 ) * (seq . 0 )) by BHSP_4:def 1

      .= (((Cseq . 0 ) + (( - (Cseq ^\ 1)) . 0 )) * (seq . 0 )) by VALUED_1: 1

      .= (((Cseq . 0 ) + ( - ((Cseq ^\ 1) . 0 ))) * (seq . 0 )) by VALUED_1: 8

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

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

      .= (((Cseq . 0 ) * (seq . 0 )) - ((Cseq . 1) * (seq . 0 ))) by CLVECT_1: 10;



       A2: ((Cseq * ( Partial_Sums seq)) . ( 0 + 1)) = ((Cseq . ( 0 + 1)) * (( Partial_Sums seq) . ( 0 + 1))) by Def8

      .= ((Cseq . ( 0 + 1)) * ((( Partial_Sums seq) . 0 ) + (seq . ( 0 + 1)))) by BHSP_4:def 1

      .= ((Cseq . 1) * ((seq . 0 ) + (seq . 1))) by BHSP_4:def 1

      .= (((Cseq . 1) * (seq . 0 )) + ((Cseq . 1) * (seq . 1))) by CLVECT_1:def 2;

       A3:

      now

        let n;

        assume P[n];

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

        then

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

        (( Partial_Sums (Cseq * seq)) . ((n + 1) + 1)) = ((( Partial_Sums (Cseq * seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1))) by BHSP_4:def 1

        .= (((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . n) + ((Cseq * ( Partial_Sums seq)) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1))) by A4, RLVECT_1: 13

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

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((Cseq . (n + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1)))) by Def8

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1))) * (( Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by Def8

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

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

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

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) + (( - (Cseq ^\ 1)) . (n + 1))) * (( Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by VALUED_1: 8

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((((Cseq - (Cseq ^\ 1)) . (n + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by VALUED_1: 1

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

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

        .= (((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . n) + (((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq)) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by Def8

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + (((Cseq . ((n + 1) + 1)) * (( Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by BHSP_4:def 1

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * ((( Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1))))) by CLVECT_1:def 2

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * (( Partial_Sums seq) . ((n + 1) + 1)))) by BHSP_4:def 1

        .= ((( Partial_Sums ((Cseq - (Cseq ^\ 1)) * ( Partial_Sums seq))) . (n + 1)) + ((Cseq * ( Partial_Sums seq)) . ((n + 1) + 1))) by Def8;

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

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

        hence P[(n + 1)] by RLVECT_1: 4;

      end;

      (( Partial_Sums (Cseq * seq)) . ( 0 + 1)) = ((( Partial_Sums (Cseq * seq)) . 0 ) + ((Cseq * seq) . ( 0 + 1))) by BHSP_4:def 1

      .= (((Cseq * seq) . 0 ) + ((Cseq * seq) . 1)) by BHSP_4:def 1

      .= (((Cseq . 0 ) * (seq . 0 )) + ((Cseq * seq) . 1)) by Def8

      .= (((Cseq . 0 ) * (seq . 0 )) + ((Cseq . 1) * (seq . 1))) by Def8;



      then (( Partial_Sums (Cseq * seq)) . ( 0 + 1)) = ((((Cseq . 0 ) * (seq . 0 )) + 09(X)) + ((Cseq . 1) * (seq . 1))) by RLVECT_1: 4

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

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

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

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

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

      then

       A5: P[ 0 ] by RLVECT_1: 4;

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

    end;

    theorem :: CLVECT_3:53



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

    proof

      let n;

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

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

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

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

      then (( Partial_Sums (Cseq * seq)) . (n + 1)) = (((Cseq * ( Partial_Sums seq)) . (n + 1)) + (( Partial_Sums (((( - 1r ) (#) (Cseq ^\ 1)) - ( - Cseq)) * ( Partial_Sums seq))) . n)) by COMSEQ_1: 11;

      then (( Partial_Sums (Cseq * seq)) . (n + 1)) = (((Cseq * ( Partial_Sums seq)) . (n + 1)) + (( Partial_Sums (((( - 1r ) (#) (Cseq ^\ 1)) - (( - 1r ) (#) Cseq)) * ( Partial_Sums seq))) . n)) by COMSEQ_1: 11;

      then (( Partial_Sums (Cseq * seq)) . (n + 1)) = (((Cseq * ( Partial_Sums seq)) . (n + 1)) + (( Partial_Sums ((( - 1r ) (#) ((Cseq ^\ 1) - Cseq)) * ( Partial_Sums seq))) . n)) by COMSEQ_1: 18;

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

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

      then (( Partial_Sums (Cseq * seq)) . (n + 1)) = (((Cseq * ( Partial_Sums seq)) . (n + 1)) + (( - 1r ) * (( Partial_Sums (((Cseq ^\ 1) - Cseq) * ( Partial_Sums seq))) . n))) by CLVECT_1:def 14;

      hence thesis by CLVECT_1: 3;

    end;

    theorem :: CLVECT_3:54

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