clopban3.miz



    begin

    theorem :: CLOPBAN3:1

    

     Th1: for X be add-associative right_zeroed right_complementable non empty CNORMSTR holds for seq be sequence of X st (for n be Nat holds (seq . n) = ( 0. X)) holds for m be Nat holds (( Partial_Sums seq) . m) = ( 0. X)

    proof

      let X be add-associative right_zeroed right_complementable non empty CNORMSTR;

      let seq be sequence of X such that

       A1: for n be Nat holds (seq . n) = ( 0. X);

      let m be Nat;

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

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A3: P[k];

        

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

        .= ((( Partial_Sums seq) . k) + (seq . (k + 1))) by A1, A3

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

      end;

      

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

      for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

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

      then seq = ( Partial_Sums seq) by FUNCT_2: 63;

      hence thesis by A1;

    end;

    definition

      let X be ComplexNormSpace;

      let seq be sequence of X;

      :: CLOPBAN3:def1

      attr seq is summable means

      : Def1: ( Partial_Sums seq) is convergent;

    end

    registration

      let X be ComplexNormSpace;

      cluster summable for sequence of X;

      existence

      proof

        reconsider C = ( NAT --> ( 0. X)) as sequence of X;

        take C;

        take ( 0. X);

        let p be Real such that

         A1: 0 < p;

        take 0 ;

        let m be Nat such that 0 <= m;

        for n be Nat holds (C . n) = ( 0. X) by ORDINAL1:def 12, FUNCOP_1: 7;

        

        then ||.((( Partial_Sums C) . m) - ( 0. X)).|| = ||.(( 0. X) - ( 0. X)).|| by Th1

        .= 0 by CLVECT_1: 107;

        hence thesis by A1;

      end;

    end

    definition

      let X be ComplexNormSpace;

      let seq be sequence of X;

      :: CLOPBAN3:def2

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

      correctness ;

    end

    definition

      let X be ComplexNormSpace;

      let seq be sequence of X;

      :: CLOPBAN3:def3

      attr seq is norm_summable means

      : Def3: ||.seq.|| is summable;

    end

    theorem :: CLOPBAN3:2

    

     Th2: for X be ComplexNormSpace, seq be sequence of X, m be Nat holds 0 <= ( ||.seq.|| . m)

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let m be Nat;

      ( ||.seq.|| . m) = ||.(seq . m).|| by NORMSP_0:def 4;

      hence thesis by CLVECT_1: 105;

    end;

    theorem :: CLOPBAN3:3

    

     Th3: for X be ComplexNormSpace, x,y,z be Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||

    proof

      let X be ComplexNormSpace;

      let x,y,z be Element of X;

      

      thus ||.(x - y).|| = ||.((x - ( 0. X)) - y).|| by RLVECT_1: 13

      .= ||.((x - (z - z)) - y).|| by RLVECT_1: 5

      .= ||.(((x - z) + z) - y).|| by RLVECT_1: 29

      .= ||.((x - z) + (z - y)).|| by RLVECT_1:def 3;

    end;

    theorem :: CLOPBAN3:4

    

     Th4: for X be ComplexNormSpace, seq be sequence of X holds seq is convergent implies for s be Real st 0 < s holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - (seq . n)).|| < s

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      assume seq is convergent;

      then

      consider g1 be Element of X such that

       A1: for s be Real st 0 < s holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - g1).|| < s;

      let s be Real;

      assume 0 < s;

      then

      consider n be Nat such that

       A2: for m be Nat st n <= m holds ||.((seq . m) - g1).|| < (s / 2) by A1;

      now

        let m be Nat;

        assume n <= m;

        then

         A3: ||.((seq . m) - g1).|| < (s / 2) by A2;

        

         A4: ||.(((seq . m) - g1) + (g1 - (seq . n))).|| <= ( ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).||) & ||.(((seq . m) - g1) + (g1 - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| by Th3, CLVECT_1:def 13;

         ||.((seq . n) - g1).|| < (s / 2) by A2;

        then ||.(g1 - (seq . n)).|| < (s / 2) by CLVECT_1: 108;

        then ( ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).||) < ((s / 2) + (s / 2)) by A3, XREAL_1: 8;

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

      end;

      hence thesis;

    end;

    theorem :: CLOPBAN3:5

    

     Th5: for X be ComplexNormSpace, seq be sequence of X holds seq is Cauchy_sequence_by_Norm iff for p be Real st p > 0 holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - (seq . n)).|| < p

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

       A1:

      now

        assume

         A2: for p be Real st p > 0 holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - (seq . n)).|| < p;

        now

          let s be Real;

          assume 0 < s;

          then

          consider k be Nat such that

           A3: for m be Nat st k <= m holds ||.((seq . m) - (seq . k)).|| < (s / 2) by A2;

          now

            let m,n be Nat such that

             A4: k <= m and

             A5: k <= n;

             ||.((seq . n) - (seq . k)).|| < (s / 2) by A3, A5;

            then

             A6: ||.((seq . k) - (seq . n)).|| < (s / 2) by CLVECT_1: 108;

             ||.((seq . m) - (seq . k)).|| < (s / 2) by A3, A4;

            then

             A7: ( ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).||) < ((s / 2) + (s / 2)) by A6, XREAL_1: 8;

             ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| <= ( ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).||) & ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| by Th3, CLVECT_1:def 13;

            hence ||.((seq . m) - (seq . n)).|| < s by A7, XXREAL_0: 2;

          end;

          hence ex k be Nat st for m,n be Nat st k <= m & k <= n holds ||.((seq . m) - (seq . n)).|| < s;

        end;

        hence seq is Cauchy_sequence_by_Norm by CSSPACE3: 8;

      end;

      now

        assume

         A8: seq is Cauchy_sequence_by_Norm;

        thus for p be Real st p > 0 holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - (seq . n)).|| < p

        proof

          let p be Real;

          assume p > 0 ;

          then

          consider n be Nat such that

           A9: for m,k be Nat st n <= m & n <= k holds ||.((seq . m) - (seq . k)).|| < p by A8, CSSPACE3: 8;

          for m be Nat st n <= m holds ||.((seq . m) - (seq . n)).|| < p by A9;

          hence thesis;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: CLOPBAN3:6

    

     Th6: for X be ComplexNormSpace, seq be sequence of X st (for n be Nat holds (seq . n) = ( 0. X)) holds for m be Nat holds (( Partial_Sums ||.seq.||) . m) = 0

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X such that

       A1: for n be Nat holds (seq . n) = ( 0. X);

      let m be Nat;

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

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A3: P[k];

        

        thus ( ||.seq.|| . (k + 1)) = ( 0 + ( ||.seq.|| . (k + 1)))

        .= ( ||.( 0. X).|| + ( ||.seq.|| . (k + 1)))

        .= ( ||.(seq . k).|| + ( ||.seq.|| . (k + 1))) by A1

        .= ((( Partial_Sums ||.seq.||) . k) + ( ||.seq.|| . (k + 1))) by A3, NORMSP_0:def 4

        .= (( Partial_Sums ||.seq.||) . (k + 1)) by SERIES_1:def 1;

      end;

      

       A4: P[ 0 ] by SERIES_1:def 1;

      for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

      

      hence (( Partial_Sums ||.seq.||) . m) = ( ||.seq.|| . m)

      .= ||.(seq . m).|| by NORMSP_0:def 4

      .= ||.( 0. X).|| by A1

      .= 0 ;

    end;

    theorem :: CLOPBAN3:7

    

     Th7: for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq1 is subsequence of seq & seq is convergent implies seq1 is convergent

    proof

      let X be ComplexNormSpace;

      let seq,seq1 be sequence of X;

      assume that

       A1: seq1 is subsequence of seq and

       A2: seq is convergent;

      consider g1 be Element of X such that

       A3: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - g1).|| < p by A2;

      take g1;

      let p be Real;

      assume 0 < p;

      then

      consider n1 be Nat such that

       A4: for m be Nat st n1 <= m holds ||.((seq . m) - g1).|| < p by A3;

      take n = n1;

      let m be Nat such that

       A5: n <= m;

      

       A6: m in NAT by ORDINAL1:def 12;

      consider Nseq be increasing sequence of NAT such that

       A7: seq1 = (seq * Nseq) by A1, VALUED_0:def 17;

      m <= (Nseq . m) by SEQM_3: 14;

      then

       A8: n <= (Nseq . m) by A5, XXREAL_0: 2;

      (seq1 . m) = (seq . (Nseq . m)) by A7, FUNCT_2: 15, A6;

      hence thesis by A4, A8;

    end;

    theorem :: CLOPBAN3:8

    

     Th8: for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq1 is subsequence of seq & seq is convergent implies ( lim seq1) = ( lim seq)

    proof

      let X be ComplexNormSpace;

      let seq,seq1 be sequence of X;

      assume that

       A1: seq1 is subsequence of seq and

       A2: seq is convergent;

      consider Nseq be increasing sequence of NAT such that

       A3: seq1 = (seq * Nseq) by A1, VALUED_0:def 17;

       A4:

      now

        let p be Real;

        assume 0 < p;

        then

        consider n1 be Nat such that

         A5: for m be Nat st n1 <= m holds ||.((seq . m) - ( lim seq)).|| < p by A2, CLVECT_1:def 16;

        take n = n1;

        let m be Nat such that

         A6: n <= m;

        

         A7: m in NAT by ORDINAL1:def 12;

        m <= (Nseq . m) by SEQM_3: 14;

        then

         A8: n <= (Nseq . m) by A6, XXREAL_0: 2;

        (seq1 . m) = (seq . (Nseq . m)) by A3, FUNCT_2: 15, A7;

        hence ||.((seq1 . m) - ( lim seq)).|| < p by A5, A8;

      end;

      seq1 is convergent by A1, A2, Th7;

      hence thesis by A4, CLVECT_1:def 16;

    end;

    theorem :: CLOPBAN3:9

    for X be ComplexNormSpace, seq,seq1 be sequence of X, k be Element of NAT holds seq is convergent implies (seq ^\ k) is convergent & ( lim (seq ^\ k)) = ( lim seq) by Th7, Th8;

    theorem :: CLOPBAN3:10

    

     Th10: for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq is convergent & (ex k be Nat st seq = (seq1 ^\ k)) implies seq1 is convergent

    proof

      let X be ComplexNormSpace;

      let seq,seq1 be sequence of X;

      assume that

       A1: seq is convergent and

       A2: ex k be Nat st seq = (seq1 ^\ k);

      consider k be Nat such that

       A3: seq = (seq1 ^\ k) by A2;

      consider g1 be Element of X such that

       A4: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - g1).|| < p by A1;

      take g1;

      let p be Real;

      assume 0 < p;

      then

      consider n1 be Nat such that

       A5: for m be Nat st n1 <= m holds ||.((seq . m) - g1).|| < p by A4;

      take n = (n1 + k);

      let m be Nat;

      assume

       A6: n <= m;

      then

      consider l be Nat such that

       A7: m = ((n1 + k) + l) by NAT_1: 10;

      reconsider l as Nat;

      (m - k) = ((n1 + l) + 0 ) by A7;

      then

      consider m1 be Nat such that

       A8: m1 = (m - k);

      now

        assume not n1 <= m1;

        then (m1 + k) < (n1 + k) by XREAL_1: 6;

        hence contradiction by A6, A8;

      end;

      then

       A9: ||.((seq . m1) - g1).|| < p by A5;

      (m1 + k) = m by A8;

      hence thesis by A3, A9, NAT_1:def 3;

    end;

    theorem :: CLOPBAN3:11

    

     Th11: for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq is convergent & (ex k be Nat st seq = (seq1 ^\ k)) implies ( lim seq1) = ( lim seq)

    proof

      let X be ComplexNormSpace;

      let seq,seq1 be sequence of X;

      assume that

       A1: seq is convergent and

       A2: ex k be Nat st seq = (seq1 ^\ k);

      consider k be Nat such that

       A3: seq = (seq1 ^\ k) by A2;

       A4:

      now

        let p be Real;

        assume 0 < p;

        then

        consider n1 be Nat such that

         A5: for m be Nat st n1 <= m holds ||.((seq . m) - ( lim seq)).|| < p by A1, CLVECT_1:def 16;

        take n = (n1 + k);

        let m be Nat;

        assume

         A6: n <= m;

        then

        consider l be Nat such that

         A7: m = ((n1 + k) + l) by NAT_1: 10;

        reconsider l as Nat;

        (m - k) = ((n1 + l) + 0 ) by A7;

        then

        consider m1 be Nat such that

         A8: m1 = (m - k);

        now

          assume not n1 <= m1;

          then (m1 + k) < (n1 + k) by XREAL_1: 6;

          hence contradiction by A6, A8;

        end;

        then

         A9: ||.((seq . m1) - ( lim seq)).|| < p by A5;

        (m1 + k) = m by A8;

        hence ||.((seq1 . m) - ( lim seq)).|| < p by A3, A9, NAT_1:def 3;

      end;

      seq1 is convergent by A1, A2, Th10;

      hence thesis by A4, CLVECT_1:def 16;

    end;

    theorem :: CLOPBAN3:12

    

     Th12: for X be ComplexNormSpace, seq be sequence of X holds seq is constant implies seq is convergent

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      assume seq is constant;

      then

      consider r be Element of X such that

       A1: for n be Nat holds (seq . n) = r by VALUED_0:def 18;

      take g = r;

      let p be Real such that

       A2: 0 < p;

      take n = 0 ;

      let m be Nat such that n <= m;

       ||.((seq . m) - g).|| = ||.(r - g).|| by A1

      .= ||.( 0. X).|| by RLVECT_1: 15

      .= 0 ;

      hence thesis by A2;

    end;

    theorem :: CLOPBAN3:13

    

     Th13: for X be ComplexNormSpace, seq be sequence of X st (for n be Nat holds (seq . n) = ( 0. X)) holds seq is norm_summable

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X such that

       A1: for n be Nat holds (seq . n) = ( 0. X);

      take 0 ;

      let p be Real such that

       A2: 0 < p;

      take 0 ;

      let m be Nat such that 0 <= m;

       |.((( Partial_Sums ||.seq.||) . m) - 0 ).| = |.( 0 - 0 ).| by A1, Th6

      .= 0 by ABSVALUE:def 1;

      hence thesis by A2;

    end;

    registration

      let X be ComplexNormSpace;

      cluster norm_summable for sequence of X;

      existence

      proof

        reconsider C = ( NAT --> ( 0. X)) as sequence of X;

        take C;

        for n be Nat holds (C . n) = ( 0. X) by ORDINAL1:def 12, FUNCOP_1: 7;

        hence thesis by Th13;

      end;

    end

    theorem :: CLOPBAN3:14

    

     Th14: for X be ComplexNormSpace, s be sequence of X holds s is summable implies s is convergent & ( lim s) = ( 0. X)

    proof

      let X be ComplexNormSpace;

      let s be sequence of X;

      assume s is summable;

      then

       A1: ( Partial_Sums s) is convergent;

      then

       A2: (( Partial_Sums s) ^\ 1) is convergent by Th7;

      ( lim (( Partial_Sums s) ^\ 1)) = ( lim ( Partial_Sums s)) by A1, Th8;

      

      then

       A3: ( lim ((( Partial_Sums s) ^\ 1) - ( Partial_Sums s))) = (( lim ( Partial_Sums s)) - ( lim ( Partial_Sums s))) by A1, A2, CLVECT_1: 120

      .= ( 0. X) by RLVECT_1: 15;

      now

        let n be Nat;

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

        then (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + ((s ^\ 1) . n)) by NAT_1:def 3;

        then ((( Partial_Sums s) ^\ 1) . n) = (((s ^\ 1) . n) + (( Partial_Sums s) . n)) by NAT_1:def 3;

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

        then (((( Partial_Sums s) ^\ 1) . n) - (( Partial_Sums s) . n)) = (((s ^\ 1) . n) + ( 0. X)) by RLVECT_1: 15;

        hence (((( Partial_Sums s) ^\ 1) . n) - (( Partial_Sums s) . n)) = ((s ^\ 1) . n) by RLVECT_1: 4;

      end;

      then

       A4: (s ^\ 1) = ((( Partial_Sums s) ^\ 1) - ( Partial_Sums s)) by NORMSP_1:def 3;

      then (s ^\ 1) is convergent by A1, A2, CLVECT_1: 114;

      hence thesis by A3, A4, Th10, Th11;

    end;

    theorem :: CLOPBAN3:15

    

     Th15: for X be ComplexNormSpace, s1,s2 be sequence of X holds (( Partial_Sums s1) + ( Partial_Sums s2)) = ( Partial_Sums (s1 + s2))

    proof

      let X be ComplexNormSpace;

      let s1,s2 be sequence of X;

       A1:

      now

        let n be Nat;

        

        thus ((( Partial_Sums s1) + ( Partial_Sums s2)) . (n + 1)) = ((( Partial_Sums s1) . (n + 1)) + (( Partial_Sums s2) . (n + 1))) by NORMSP_1:def 2

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) + (( Partial_Sums s2) . (n + 1))) by BHSP_4:def 1

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) + ((s2 . (n + 1)) + (( Partial_Sums s2) . n))) by BHSP_4:def 1

        .= ((((( Partial_Sums s1) . n) + (s1 . (n + 1))) + (s2 . (n + 1))) + (( Partial_Sums s2) . n)) by RLVECT_1:def 3

        .= (((( Partial_Sums s1) . n) + ((s1 . (n + 1)) + (s2 . (n + 1)))) + (( Partial_Sums s2) . n)) by RLVECT_1:def 3

        .= (((( Partial_Sums s1) . n) + ((s1 + s2) . (n + 1))) + (( Partial_Sums s2) . n)) by NORMSP_1:def 2

        .= (((( Partial_Sums s1) . n) + (( Partial_Sums s2) . n)) + ((s1 + s2) . (n + 1))) by RLVECT_1:def 3

        .= (((( Partial_Sums s1) + ( Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1))) by NORMSP_1:def 2;

      end;

      ((( Partial_Sums s1) + ( Partial_Sums s2)) . 0 ) = ((( Partial_Sums s1) . 0 ) + (( Partial_Sums s2) . 0 )) by NORMSP_1:def 2

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

      .= ((s1 . 0 ) + (s2 . 0 )) by BHSP_4:def 1

      .= ((s1 + s2) . 0 ) by NORMSP_1:def 2;

      hence thesis by A1, BHSP_4:def 1;

    end;

    theorem :: CLOPBAN3:16

    

     Th16: for X be ComplexNormSpace, s1,s2 be sequence of X holds (( Partial_Sums s1) - ( Partial_Sums s2)) = ( Partial_Sums (s1 - s2))

    proof

      let X be ComplexNormSpace;

      let s1,s2 be sequence of X;

       A1:

      now

        let n be Nat;

        

        thus ((( Partial_Sums s1) - ( Partial_Sums s2)) . (n + 1)) = ((( Partial_Sums s1) . (n + 1)) - (( Partial_Sums s2) . (n + 1))) by NORMSP_1:def 3

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) - (( Partial_Sums s2) . (n + 1))) by BHSP_4:def 1

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + (( Partial_Sums s2) . n))) by BHSP_4:def 1

        .= ((((( Partial_Sums s1) . n) + (s1 . (n + 1))) - (s2 . (n + 1))) - (( Partial_Sums s2) . n)) by RLVECT_1: 27

        .= (((( Partial_Sums s1) . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - (( Partial_Sums s2) . n)) by RLVECT_1:def 3

        .= ((((s1 - s2) . (n + 1)) + (( Partial_Sums s1) . n)) - (( Partial_Sums s2) . n)) by NORMSP_1:def 3

        .= (((s1 - s2) . (n + 1)) + ((( Partial_Sums s1) . n) - (( Partial_Sums s2) . n))) by RLVECT_1:def 3

        .= (((( Partial_Sums s1) - ( Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1))) by NORMSP_1:def 3;

      end;

      ((( Partial_Sums s1) - ( Partial_Sums s2)) . 0 ) = ((( Partial_Sums s1) . 0 ) - (( Partial_Sums s2) . 0 )) by NORMSP_1:def 3

      .= ((s1 . 0 ) - (( Partial_Sums s2) . 0 )) by BHSP_4:def 1

      .= ((s1 . 0 ) - (s2 . 0 )) by BHSP_4:def 1

      .= ((s1 - s2) . 0 ) by NORMSP_1:def 3;

      hence thesis by A1, BHSP_4:def 1;

    end;

    registration

      let X be ComplexNormSpace;

      let seq be norm_summable sequence of X;

      cluster ||.seq.|| -> summable;

      coherence by Def3;

    end

    registration

      let X be ComplexNormSpace;

      cluster summable -> convergent for sequence of X;

      coherence by Th14;

    end

    theorem :: CLOPBAN3:17

    

     Th17: for X be ComplexNormSpace, seq1,seq2 be sequence of X st seq1 is summable & seq2 is summable holds (seq1 + seq2) is summable & ( Sum (seq1 + seq2)) = (( Sum seq1) + ( Sum seq2))

    proof

      let X be ComplexNormSpace;

      let seq1,seq2 be sequence of X;

      assume seq1 is summable & seq2 is summable;

      then

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

      then

       A2: (( Partial_Sums seq1) + ( Partial_Sums seq2)) is convergent by CLVECT_1: 113;

      

       A3: (( Partial_Sums seq1) + ( Partial_Sums seq2)) = ( Partial_Sums (seq1 + seq2)) by Th15;

      ( Sum (seq1 + seq2)) = ( lim (( Partial_Sums seq1) + ( Partial_Sums seq2))) by Th15

      .= (( lim ( Partial_Sums seq1)) + ( lim ( Partial_Sums seq2))) by A1, CLVECT_1: 119;

      hence thesis by A2, A3;

    end;

    theorem :: CLOPBAN3:18

    

     Th18: for X be ComplexNormSpace, seq1,seq2 be sequence of X st seq1 is summable & seq2 is summable holds (seq1 - seq2) is summable & ( Sum (seq1 - seq2)) = (( Sum seq1) - ( Sum seq2))

    proof

      let X be ComplexNormSpace;

      let seq1,seq2 be sequence of X;

      assume seq1 is summable & seq2 is summable;

      then

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

      then

       A2: (( Partial_Sums seq1) - ( Partial_Sums seq2)) is convergent by CLVECT_1: 114;

      

       A3: (( Partial_Sums seq1) - ( Partial_Sums seq2)) = ( Partial_Sums (seq1 - seq2)) by Th16;

      ( Sum (seq1 - seq2)) = ( lim (( Partial_Sums seq1) - ( Partial_Sums seq2))) by Th16

      .= (( lim ( Partial_Sums seq1)) - ( lim ( Partial_Sums seq2))) by A1, CLVECT_1: 120;

      hence thesis by A2, A3;

    end;

    registration

      let X be ComplexNormSpace;

      let seq1,seq2 be summable sequence of X;

      cluster (seq1 + seq2) -> summable;

      coherence by Th17;

      cluster (seq1 - seq2) -> summable;

      coherence by Th18;

    end

    theorem :: CLOPBAN3:19

    

     Th19: for X be ComplexNormSpace, seq be sequence of X, z be Complex holds ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq))

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let z be Complex;

      defpred P[ Nat] means (( Partial_Sums (z * seq)) . $1) = ((z * ( Partial_Sums seq)) . $1);

       A1:

      now

        let n be Nat;

        assume

         A2: P[n];

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

        .= ((z * (( Partial_Sums seq) . n)) + ((z * seq) . (n + 1))) by A2, CLVECT_1:def 14

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

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

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

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

        hence P[(n + 1)];

      end;

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

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

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

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

      then

       A3: P[ 0 ];

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

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

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLOPBAN3:20

    

     Th20: for X be ComplexNormSpace, seq be summable sequence of X, z be Complex holds (z * seq) is summable & ( Sum (z * seq)) = (z * ( Sum seq))

    proof

      let X be ComplexNormSpace;

      let seq be summable sequence of X;

      let z be Complex;

      

       A1: ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq)) by Th19;

      

       A2: ( Partial_Sums seq) is convergent by Def1;

      then

       A3: (z * ( Partial_Sums seq)) is convergent by CLVECT_1: 116;

      ( Sum (z * seq)) = ( lim (z * ( Partial_Sums seq))) by Th19

      .= (z * ( Sum seq)) by A2, CLVECT_1: 122;

      hence thesis by A3, A1;

    end;

    registration

      let X be ComplexNormSpace;

      let z be Complex, seq be summable sequence of X;

      cluster (z * seq) -> summable;

      coherence by Th20;

    end

    theorem :: CLOPBAN3:21

    

     Th21: for X be ComplexNormSpace, s,s1 be sequence of X st for n be Nat holds (s1 . n) = (s . 0 ) holds ( Partial_Sums (s ^\ 1)) = ((( Partial_Sums s) ^\ 1) - s1)

    proof

      let X be ComplexNormSpace;

      let s,s1 be sequence of X;

      assume

       A1: for n be Nat holds (s1 . n) = (s . 0 );

       A2:

      now

        let k be Nat;

        

        thus (((( Partial_Sums s) ^\ 1) - s1) . (k + 1)) = (((( Partial_Sums s) ^\ 1) . (k + 1)) - (s1 . (k + 1))) by NORMSP_1:def 3

        .= (((( Partial_Sums s) ^\ 1) . (k + 1)) - (s . 0 )) by A1

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

        .= (((s . ((k + 1) + 1)) + (( Partial_Sums s) . (k + 1))) - (s . 0 )) by BHSP_4:def 1

        .= (((s . ((k + 1) + 1)) + (( Partial_Sums s) . (k + 1))) - (s1 . k)) by A1

        .= ((s . ((k + 1) + 1)) + ((( Partial_Sums s) . (k + 1)) - (s1 . k))) by RLVECT_1:def 3

        .= ((s . ((k + 1) + 1)) + (((( Partial_Sums s) ^\ 1) . k) - (s1 . k))) by NAT_1:def 3

        .= ((s . ((k + 1) + 1)) + (((( Partial_Sums s) ^\ 1) - s1) . k)) by NORMSP_1:def 3

        .= ((((( Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))) by NAT_1:def 3;

      end;

      (((( Partial_Sums s) ^\ 1) - s1) . 0 ) = (((( Partial_Sums s) ^\ 1) . 0 ) - (s1 . 0 )) by NORMSP_1:def 3

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

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

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

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

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

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

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

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

      hence thesis by A2, BHSP_4:def 1;

    end;

    theorem :: CLOPBAN3:22

    

     Th22: for X be ComplexNormSpace, s be sequence of X holds s is summable implies for n be Nat holds (s ^\ n) is summable

    proof

      let X be ComplexNormSpace;

      let s be sequence of X;

      defpred X[ Nat] means (s ^\ $1) is summable;

      

       A1: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        reconsider s1 = ( NAT --> ((s ^\ n) . 0 )) as sequence of X;

        for k be Nat holds (s1 . k) = ((s ^\ n) . 0 ) by ORDINAL1:def 12, FUNCOP_1: 7;

        then

         A2: ( Partial_Sums ((s ^\ n) ^\ 1)) = ((( Partial_Sums (s ^\ n)) ^\ 1) - s1) by Th21;

        assume (s ^\ n) is summable;

        then ( Partial_Sums (s ^\ n)) is convergent;

        then

         A3: (( Partial_Sums (s ^\ n)) ^\ 1) is convergent by Th7;

        s1 is convergent by Th12;

        then (s ^\ (n + 1)) = ((s ^\ n) ^\ 1) & ( Partial_Sums ((s ^\ n) ^\ 1)) is convergent by A3, A2, CLVECT_1: 114, NAT_1: 48;

        hence thesis by Def1;

      end;

      assume s is summable;

      then

       A4: X[ 0 ] by NAT_1: 47;

      thus for n be Nat holds X[n] from NAT_1:sch 2( A4, A1);

    end;

    registration

      let X be ComplexNormSpace;

      let seq be summable sequence of X, n be Nat;

      cluster (seq ^\ n) -> summable;

      coherence by Th22;

    end

    theorem :: CLOPBAN3:23

    

     Th23: for X be ComplexNormSpace, seq be sequence of X holds ( Partial_Sums ||.seq.||) is bounded_above iff seq is norm_summable

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      for n be Nat holds 0 <= ( ||.seq.|| . n) by Th2;

      then ( Partial_Sums ||.seq.||) is bounded_above iff ||.seq.|| is summable by SERIES_1: 17;

      hence thesis;

    end;

    registration

      let X be ComplexNormSpace;

      let seq be norm_summable sequence of X;

      cluster ( Partial_Sums ||.seq.||) -> bounded_above;

      coherence by Th23;

    end

    theorem :: CLOPBAN3:24

    

     Th24: for X be ComplexBanachSpace, seq be sequence of X holds seq is summable iff for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ||.((( Partial_Sums seq) . m) - (( Partial_Sums seq) . n)).|| < p by Th5, CLOPBAN1:def 13, Th4;

    theorem :: CLOPBAN3:25

    

     Th25: for X be ComplexNormSpace, s be sequence of X, n,m be Nat st n <= m holds ||.((( Partial_Sums s) . m) - (( Partial_Sums s) . n)).|| <= |.((( Partial_Sums ||.s.||) . m) - (( Partial_Sums ||.s.||) . n)).|

    proof

      let X be ComplexNormSpace;

      let s be sequence of X;

      set s1 = ( Partial_Sums s);

      set s2 = ( Partial_Sums ||.s.||);

      let n,m be Nat;

      assume n <= m;

      then

      reconsider k = (m - n) as Element of NAT by INT_1: 5;

      defpred X[ Nat] means ||.((s1 . (n + $1)) - (s1 . n)).|| <= |.((s2 . (n + $1)) - (s2 . n)).|;

      

       A1: (n + k) = m;

      now

        let k be Nat;

         ||.(s . k).|| >= 0 by CLVECT_1: 105;

        hence ( ||.s.|| . k) >= 0 by NORMSP_0:def 4;

      end;

      then

       A2: s2 is non-decreasing by SERIES_1: 16;

      

       A3: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        

         A4: |.((s2 . (n + (k + 1))) - (s2 . n)).| = |.(((s2 . (n + k)) + ( ||.s.|| . ((n + k) + 1))) - (s2 . n)).| by SERIES_1:def 1

        .= |.(((s2 . (n + k)) + ||.(s . ((n + k) + 1)).||) - (s2 . n)).| by NORMSP_0:def 4

        .= |.( ||.(s . ((n + k) + 1)).|| + ((s2 . (n + k)) - (s2 . n))).|;

         ||.((s1 . (n + (k + 1))) - (s1 . n)).|| = ||.(((s . ((n + k) + 1)) + (s1 . (n + k))) - (s1 . n)).|| by BHSP_4:def 1

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

        then

         A5: ||.((s1 . (n + (k + 1))) - (s1 . n)).|| <= ( ||.(s . ((n + k) + 1)).|| + ||.((s1 . (n + k)) - (s1 . n)).||) by CLVECT_1:def 13;

        (s2 . (n + k)) >= (s2 . n) by A2, SEQM_3: 5;

        then

         A6: ((s2 . (n + k)) - (s2 . n)) >= 0 by XREAL_1: 48;

        assume ||.((s1 . (n + k)) - (s1 . n)).|| <= |.((s2 . (n + k)) - (s2 . n)).|;

        then ( ||.(s . ((n + k) + 1)).|| + ||.((s1 . (n + k)) - (s1 . n)).||) <= ( ||.(s . ((n + k) + 1)).|| + |.((s2 . (n + k)) - (s2 . n)).|) by XREAL_1: 7;

        then ||.((s1 . (n + (k + 1))) - (s1 . n)).|| <= ( ||.(s . ((n + k) + 1)).|| + |.((s2 . (n + k)) - (s2 . n)).|) by A5, XXREAL_0: 2;

        then

         A7: ||.((s1 . (n + (k + 1))) - (s1 . n)).|| <= ( ||.(s . ((n + k) + 1)).|| + ((s2 . (n + k)) - (s2 . n))) by A6, ABSVALUE:def 1;

         ||.(s . ((n + k) + 1)).|| >= 0 by CLVECT_1: 105;

        hence thesis by A6, A7, A4, ABSVALUE:def 1;

      end;

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

      .= 0 ;

      then

       A8: X[ 0 ] by COMPLEX1: 46;

      for k be Nat holds X[k] from NAT_1:sch 2( A8, A3);

      hence thesis by A1;

    end;

    theorem :: CLOPBAN3:26

    

     Th26: for X be ComplexBanachSpace, seq be sequence of X holds seq is norm_summable implies seq is summable

    proof

      let X be ComplexBanachSpace;

      let seq be sequence of X;

      assume seq is norm_summable;

      then

       A1: ( Partial_Sums ||.seq.||) is convergent by SERIES_1:def 2;

      now

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         A2: for m be Nat st n <= m holds |.((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . n)).| < p by A1, SEQ_4: 41;

        take n;

        let m be Nat;

        assume

         A3: n <= m;

        then

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

         |.((( Partial_Sums ||.seq.||) . m) - (( Partial_Sums ||.seq.||) . n)).| < p by A2, A3;

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

      end;

      hence thesis by Th24;

    end;

    theorem :: CLOPBAN3:27

    for X be ComplexNormSpace, rseq1 be Real_Sequence, seq2 be sequence of X holds rseq1 is summable & (ex m be Nat st for n be Nat st m <= n holds ||.(seq2 . n).|| <= (rseq1 . n)) implies seq2 is norm_summable

    proof

      let X be ComplexNormSpace;

      let rseq1 be Real_Sequence;

      let seq2 be sequence of X;

      assume that

       A1: rseq1 is summable and

       A2: ex m be Nat st for n be Nat st m <= n holds ||.(seq2 . n).|| <= (rseq1 . n);

      consider m be Nat such that

       A3: for n be Nat st m <= n holds ||.(seq2 . n).|| <= (rseq1 . n) by A2;

       A4:

      now

        let n be Nat;

         ||.(seq2 . n).|| = ( ||.seq2.|| . n) by NORMSP_0:def 4;

        hence 0 <= ( ||.seq2.|| . n) by CLVECT_1: 105;

      end;

      now

        let n be Nat;

        assume m <= n;

        then ||.(seq2 . n).|| <= (rseq1 . n) by A3;

        hence ( ||.seq2.|| . n) <= (rseq1 . n) by NORMSP_0:def 4;

      end;

      hence ||.seq2.|| is summable by A1, A4, SERIES_1: 19;

    end;

    theorem :: CLOPBAN3:28

    for X be ComplexNormSpace, seq1,seq2 be sequence of X holds (for n be Nat holds 0 <= ( ||.seq1.|| . n) & ( ||.seq1.|| . n) <= ( ||.seq2.|| . n)) & seq2 is norm_summable implies seq1 is norm_summable & ( Sum ||.seq1.||) <= ( Sum ||.seq2.||) by SERIES_1: 20;

    theorem :: CLOPBAN3:29

    for X be ComplexNormSpace, seq be sequence of X holds (for n be Nat holds ( ||.seq.|| . n) > 0 ) & (ex m be Nat st for n be Nat st n >= m holds (( ||.seq.|| . (n + 1)) / ( ||.seq.|| . n)) >= 1) implies not seq is norm_summable by SERIES_1: 27;

    theorem :: CLOPBAN3:30

    for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds (rseq1 . n) = (n -root ( ||.seq.|| . n))) & rseq1 is convergent & ( lim rseq1) < 1 implies seq is norm_summable

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let rseq1 be Real_Sequence;

      assume

       A1: (for n be Nat holds (rseq1 . n) = (n -root ( ||.seq.|| . n))) & rseq1 is convergent & ( lim rseq1) < 1;

      for n be Nat holds ( ||.seq.|| . n) >= 0 by Th2;

      hence ||.seq.|| is summable by A1, SERIES_1: 28;

    end;

    theorem :: CLOPBAN3:31

    for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds (rseq1 . n) = (n -root ( ||.seq.|| . n))) & (ex m be Nat st for n be Nat st m <= n holds (rseq1 . n) >= 1) implies not ||.seq.|| is summable

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let rseq1 be Real_Sequence;

      assume

       A1: (for n be Nat holds (rseq1 . n) = (n -root ( ||.seq.|| . n))) & ex m be Nat st for n be Nat st m <= n holds (rseq1 . n) >= 1;

      for n be Nat holds ( ||.seq.|| . n) >= 0 by Th2;

      hence thesis by A1, SERIES_1: 29;

    end;

    theorem :: CLOPBAN3:32

    for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds (rseq1 . n) = (n -root ( ||.seq.|| . n))) & rseq1 is convergent & ( lim rseq1) > 1 implies not seq is norm_summable

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let rseq1 be Real_Sequence;

      assume

       A1: (for n be Nat holds (rseq1 . n) = (n -root ( ||.seq.|| . n))) & rseq1 is convergent & ( lim rseq1) > 1;

      for n be Nat holds ( ||.seq.|| . n) >= 0 by Th2;

      hence not ||.seq.|| is summable by A1, SERIES_1: 30;

    end;

    theorem :: CLOPBAN3:33

    for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence st ||.seq.|| is non-increasing & (for n be Nat holds (rseq1 . n) = ((2 to_power n) * ( ||.seq.|| . (2 to_power n)))) holds (seq is norm_summable iff rseq1 is summable)

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let rseq1 be Real_Sequence;

      assume ||.seq.|| is non-increasing & for n be Nat holds (rseq1 . n) = ((2 to_power n) * ( ||.seq.|| . (2 to_power n)));

      then for n be Nat holds ||.seq.|| is non-increasing & ( ||.seq.|| . n) >= 0 & (rseq1 . n) = ((2 to_power n) * ( ||.seq.|| . (2 to_power n))) by Th2;

      then ||.seq.|| is summable iff rseq1 is summable by SERIES_1: 31;

      hence thesis;

    end;

    theorem :: CLOPBAN3:34

    for X be ComplexNormSpace, seq be sequence of X, p be Real st p > 1 & (for n be Nat st n >= 1 holds ( ||.seq.|| . n) = (1 / (n to_power p))) holds seq is norm_summable by SERIES_1: 32;

    theorem :: CLOPBAN3:35

    for X be ComplexNormSpace, seq be sequence of X, p be Real holds p <= 1 & (for n be Nat st n >= 1 holds ( ||.seq.|| . n) = (1 / (n to_power p))) implies not seq is norm_summable by SERIES_1: 33;

    theorem :: CLOPBAN3:36

    for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds (seq . n) <> ( 0. X) & (rseq1 . n) = (( ||.seq.|| . (n + 1)) / ( ||.seq.|| . n))) & rseq1 is convergent & ( lim rseq1) < 1 implies seq is norm_summable

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      let rseq1 be Real_Sequence;

      assume that

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

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

      now

        let n be Nat;

        

         A3: 0 <= ( ||.seq.|| . n) by Th2;

        

         A4: 0 <= ( ||.seq.|| . (n + 1)) by Th2;

        

         A5: (( abs ||.seq.||) . (n + 1)) = |.( ||.seq.|| . (n + 1)).| by SEQ_1: 12

        .= ( ||.seq.|| . (n + 1)) by A4, ABSVALUE:def 1;

        

         A6: (seq . n) <> ( 0. X) & ( ||.seq.|| . n) = ||.(seq . n).|| by A1, NORMSP_0:def 4;

        (( abs ||.seq.||) . n) = |.( ||.seq.|| . n).| by SEQ_1: 12

        .= ( ||.seq.|| . n) by A3, ABSVALUE:def 1;

        hence ( ||.seq.|| . n) <> 0 & (rseq1 . n) = ((( abs ||.seq.||) . (n + 1)) / (( abs ||.seq.||) . n)) by A1, A5, A6, NORMSP_0:def 5;

      end;

      then ||.seq.|| is absolutely_summable by A2, SERIES_1: 37;

      then

       A7: ( abs ||.seq.||) is summable;

      now

        let n be Element of NAT ;

        

         A8: 0 <= ( ||.seq.|| . n) by Th2;

        

        thus (( abs ||.seq.||) . n) = |.( ||.seq.|| . n).| by SEQ_1: 12

        .= ( ||.seq.|| . n) by A8, ABSVALUE:def 1;

      end;

      then ( abs ||.seq.||) = ||.seq.|| by FUNCT_2: 63;

      hence thesis by A7;

    end;

    theorem :: CLOPBAN3:37

    for X be ComplexNormSpace, seq be sequence of X holds (for n be Nat holds (seq . n) <> ( 0. X)) & (ex m be Nat st for n be Nat st n >= m holds (( ||.seq.|| . (n + 1)) / ( ||.seq.|| . n)) >= 1) implies not seq is norm_summable

    proof

      let X be ComplexNormSpace;

      let seq be sequence of X;

      assume that

       A1: for n be Nat holds (seq . n) <> ( 0. X) and

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

      consider m be Nat such that

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

       A4:

      now

        let n be Nat such that

         A5: n >= m;

        

         A6: 0 <= ( ||.seq.|| . n) by Th2;

        

         A7: 0 <= ( ||.seq.|| . (n + 1)) by Th2;

        

         A8: (( abs ||.seq.||) . (n + 1)) = |.( ||.seq.|| . (n + 1)).| by SEQ_1: 12

        .= ( ||.seq.|| . (n + 1)) by A7, ABSVALUE:def 1;

        (( abs ||.seq.||) . n) = |.( ||.seq.|| . n).| by SEQ_1: 12

        .= ( ||.seq.|| . n) by A6, ABSVALUE:def 1;

        hence ((( abs ||.seq.||) . (n + 1)) / (( abs ||.seq.||) . n)) >= 1 by A3, A5, A8;

      end;

      now

        let n be Nat;

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

        then ||.(seq . n).|| <> 0 by NORMSP_0:def 5;

        hence ( ||.seq.|| . n) <> 0 by NORMSP_0:def 4;

      end;

      hence not ||.seq.|| is summable by A4, SERIES_1: 39;

    end;

    registration

      let X be ComplexBanachSpace;

      cluster norm_summable -> summable for sequence of X;

      coherence by Th26;

    end

    begin

    theorem :: CLOPBAN3:38

    

     Th38: for X be Complex_Banach_Algebra holds for x,y,z be Element of X, a,b be Complex holds (a * (x * y)) = ((a * x) * y) & (a * (x + y)) = ((a * x) + (a * y)) & ((a + b) * x) = ((a * x) + (b * x)) & ((a * b) * x) = (a * (b * x)) & ((a * b) * (x * y)) = ((a * x) * (b * y)) & (a * (x * y)) = (x * (a * y)) & (( 0. X) * x) = ( 0. X) & (x * ( 0. X)) = ( 0. X) & (x * (y - z)) = ((x * y) - (x * z)) & ((y - z) * x) = ((y * x) - (z * x)) & ((x + y) - z) = (x + (y - z)) & ((x - y) + z) = (x - (y - z)) & ((x - y) - z) = (x - (y + z)) & (x + y) = ((x - z) + (z + y)) & (x - y) = ((x - z) + (z - y)) & x = ((x - y) + y) & x = (y - (y - x)) & ( ||.x.|| = 0 iff x = ( 0. X)) & ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(x * y).|| <= ( ||.x.|| * ||.y.||) & ||.( 1. X).|| = 1

    proof

      let X be Complex_Banach_Algebra;

      let x,y,z be Element of X;

      let a,b be Complex;

      thus (a * (x * y)) = ((a * x) * y) & (a * (x + y)) = ((a * x) + (a * y)) & ((a + b) * x) = ((a * x) + (b * x)) & ((a * b) * x) = (a * (b * x)) by CFUNCDOM:def 9, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4;

      

      thus ((a * b) * (x * y)) = (a * (b * (x * y))) by CLVECT_1:def 4

      .= (a * (x * (b * y))) by CLOPBAN2:def 11

      .= ((a * x) * (b * y)) by CFUNCDOM:def 9;

      thus (a * (x * y)) = (x * (a * y)) by CLOPBAN2:def 11;

      

       A1: ((x * (y - z)) + (x * z)) = (x * ((y - z) + z)) by VECTSP_1:def 2

      .= (x * (y - (z - z))) by RLVECT_1: 29

      .= (x * (y - ( 0. X))) by RLVECT_1: 15

      .= (x * y) by RLVECT_1: 13;

      (x * ( 0. X)) = (x * (( 0. X) + ( 0. X))) by RLVECT_1:def 4

      .= ((x * ( 0. X)) + (x * ( 0. X))) by VECTSP_1:def 2;

      then ( 0. X) = (((x * ( 0. X)) + (x * ( 0. X))) - (x * ( 0. X))) by RLVECT_1: 15;

      then ( 0. X) = ((x * ( 0. X)) + ((x * ( 0. X)) - (x * ( 0. X)))) by RLVECT_1:def 3;

      then

       A2: ( 0. X) = ((x * ( 0. X)) + ( 0. X)) by RLVECT_1: 15;

      (( 0. X) * x) = ((( 0. X) + ( 0. X)) * x) by RLVECT_1:def 4

      .= ((( 0. X) * x) + (( 0. X) * x)) by VECTSP_1:def 3;

      then ( 0. X) = (((( 0. X) * x) + (( 0. X) * x)) - (( 0. X) * x)) by RLVECT_1: 15;

      then ( 0. X) = ((( 0. X) * x) + ((( 0. X) * x) - (( 0. X) * x))) by RLVECT_1:def 3;

      then ( 0. X) = ((( 0. X) * x) + ( 0. X)) by RLVECT_1: 15;

      hence (( 0. X) * x) = ( 0. X) & (x * ( 0. X)) = ( 0. X) by A2, RLVECT_1:def 4;

      

      thus (x * (y - z)) = ((x * (y - z)) + ( 0. X)) by RLVECT_1: 4

      .= ((x * (y - z)) + ((x * z) - (x * z))) by RLVECT_1: 15

      .= ((x * y) - (x * z)) by A1, RLVECT_1:def 3;

      

       A3: (((y - z) * x) + (z * x)) = (((y - z) + z) * x) by VECTSP_1:def 3

      .= ((y - (z - z)) * x) by RLVECT_1: 29

      .= ((y - ( 0. X)) * x) by RLVECT_1: 15

      .= (y * x) by RLVECT_1: 13;

      

      thus ((y - z) * x) = (((y - z) * x) + ( 0. X)) by RLVECT_1: 4

      .= (((y - z) * x) + ((z * x) - (z * x))) by RLVECT_1: 15

      .= ((y * x) - (z * x)) by A3, RLVECT_1:def 3;

      thus ((x + y) - z) = (x + (y - z)) by RLVECT_1:def 3;

      thus ((x - y) + z) = (x - (y - z)) by RLVECT_1: 29;

      thus ((x - y) - z) = (x - (y + z)) by RLVECT_1: 27;

      

      thus ((x - z) + (z + y)) = (((x - z) + z) + y) by RLVECT_1:def 3

      .= ((x - (z - z)) + y) by RLVECT_1: 29

      .= ((x - ( 0. X)) + y) by RLVECT_1: 15

      .= (x + y) by RLVECT_1: 13;

      

      thus ((x - z) + (z - y)) = (((x - z) + z) - y) by RLVECT_1:def 3

      .= ((x - (z - z)) - y) by RLVECT_1: 29

      .= ((x - ( 0. X)) - y) by RLVECT_1: 15

      .= (x - y) by RLVECT_1: 13;

      

      thus ((x - y) + y) = (x - (y - y)) by RLVECT_1: 29

      .= (x - ( 0. X)) by RLVECT_1: 15

      .= x by RLVECT_1: 13;

      

      thus (y - (y - x)) = ((y - y) + x) by RLVECT_1: 29

      .= (( 0. X) + x) by RLVECT_1: 15

      .= x by RLVECT_1: 4;

      thus ( ||.x.|| = 0 iff x = ( 0. X)) & ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(x * y).|| <= ( ||.x.|| * ||.y.||) by CLOPBAN2:def 9, CLVECT_1:def 13, NORMSP_0:def 5;

      thus ||.( 1. X).|| = 1 by CLOPBAN2:def 10;

    end;

    registration

      cluster -> well-unital for Complex_Banach_Algebra;

      coherence

      proof

        let X be Complex_Banach_Algebra;

        let x be Element of X;

        thus thesis by VECTSP_1:def 4, VECTSP_1:def 8;

      end;

    end

    definition

      ::$Canceled

    end

    definition

      let X be Complex_Banach_Algebra;

      let z be Element of X;

      :: CLOPBAN3:def7

      func z GeoSeq -> sequence of X means

      : Def4: (it . 0 ) = ( 1. X) & for n be Nat holds (it . (n + 1)) = ((it . n) * z);

      existence

      proof

        deffunc G( set, set) = (the multF of X . [$2, z]);

        consider g be Function such that

         A1: ( dom g) = NAT & (g . 0 ) = ( 1. X) & for n be Nat holds (g . (n + 1)) = G(n,.) from NAT_1:sch 11;

        defpred P[ Nat] means (g . $1) in the carrier of X;

        

         A2: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume P[k];

          then

          reconsider gk = (g . k) as Element of X;

          (g . (k + 1)) = (the multF of X . [gk, z]) by A1;

          hence thesis;

        end;

        

         A3: P[ 0 ] by A1;

        for n be Nat holds P[n] from NAT_1:sch 2( A3, A2);

        then for n be object st n in NAT holds (g . n) in the carrier of X;

        then

        reconsider g0 = g as sequence of X by A1, FUNCT_2: 3;

        take g0;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let seq1,seq2 be sequence of X;

        assume that

         A4: (seq1 . 0 ) = ( 1. X) and

         A5: for n be Nat holds (seq1 . (n + 1)) = ((seq1 . n) * z) and

         A6: (seq2 . 0 ) = ( 1. X) and

         A7: for n be Nat holds (seq2 . (n + 1)) = ((seq2 . n) * z);

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

        

         A8: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume P[k];

          

          hence (seq1 . (k + 1)) = ((seq2 . k) * z) by A5

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

        end;

        

         A9: P[ 0 ] by A4, A6;

        for n be Nat holds P[n] from NAT_1:sch 2( A9, A8);

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

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let X be Complex_Banach_Algebra;

      let z be Element of X, n be Nat;

      :: CLOPBAN3:def8

      func z #N n -> Element of X equals ((z GeoSeq ) . n);

      correctness ;

    end

    theorem :: CLOPBAN3:39

    for X be Complex_Banach_Algebra, z be Element of X holds (z #N 0 ) = ( 1. X) by Def4;

    theorem :: CLOPBAN3:40

    

     Th40: for X be Complex_Banach_Algebra, z be Element of X holds ||.z.|| < 1 implies (z GeoSeq ) is summable norm_summable

    proof

      let X be Complex_Banach_Algebra;

      let z be Element of X;

      

       A1: 0 <= ||.z.|| by CLVECT_1: 105;

      

       A2: for n be Nat holds 0 <= ( ||.(z GeoSeq ).|| . n) & ( ||.(z GeoSeq ).|| . n) <= (( ||.z.|| GeoSeq ) . n)

      proof

        defpred P[ Nat] means 0 <= ( ||.(z GeoSeq ).|| . $1) & ( ||.(z GeoSeq ).|| . $1) <= (( ||.z.|| GeoSeq ) . $1);

        

         A3: ( ||.(z GeoSeq ).|| . 0 ) = ||.((z GeoSeq ) . 0 ).|| by NORMSP_0:def 4;

        

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

        proof

          let k be Nat;

          

           A5: 0 <= ||.z.|| by CLVECT_1: 105;

           ||.(((z GeoSeq ) . k) * z).|| <= ( ||.((z GeoSeq ) . k).|| * ||.z.||) by CLOPBAN2:def 9;

          then

           A6: ||.(((z GeoSeq ) . k) * z).|| <= (( ||.(z GeoSeq ).|| . k) * ||.z.||) by NORMSP_0:def 4;

          assume P[k];

          then (( ||.(z GeoSeq ).|| . k) * ||.z.||) <= ((( ||.z.|| GeoSeq ) . k) * ||.z.||) by A5, XREAL_1: 64;

          then

           A7: ||.(((z GeoSeq ) . k) * z).|| <= ((( ||.z.|| GeoSeq ) . k) * ||.z.||) by A6, XXREAL_0: 2;

          ( ||.(z GeoSeq ).|| . (k + 1)) = ||.((z GeoSeq ) . (k + 1)).|| by NORMSP_0:def 4

          .= ||.(((z GeoSeq ) . k) * z).|| by Def4;

          hence thesis by A7, CLVECT_1: 105, PREPOWER: 3;

        end;

         ||.((z GeoSeq ) . 0 ).|| = ||.( 1. X).|| by Def4

        .= 1 by CLOPBAN2:def 10

        .= (( ||.z.|| GeoSeq ) . 0 ) by PREPOWER: 3;

        then

         A8: P[ 0 ] by A3, CLVECT_1: 105;

        for n be Nat holds P[n] from NAT_1:sch 2( A8, A4);

        hence thesis;

      end;

      assume ||.z.|| < 1;

      then |. ||.z.||.| < 1 by A1, ABSVALUE:def 1;

      then ( ||.z.|| GeoSeq ) is summable by SERIES_1: 24;

      then ||.(z GeoSeq ).|| is summable by A2, SERIES_1: 20;

      then (z GeoSeq ) is norm_summable;

      hence thesis;

    end;

    theorem :: CLOPBAN3:41

    for X be Complex_Banach_Algebra, x be Point of X st ||.(( 1. X) - x).|| < 1 holds ((( 1. X) - x) GeoSeq ) is summable & ((( 1. X) - x) GeoSeq ) is norm_summable by Th40;

    

     Lm1: for X be ComplexNormSpace, x be Point of X st for e be Real st e > 0 holds ||.x.|| < e holds x = ( 0. X)

    proof

      let X be ComplexNormSpace;

      let x be Point of X such that

       A1: for e be Real st e > 0 holds ||.x.|| < e;

      now

        assume x <> ( 0. X);

        then 0 <> ||.x.|| by NORMSP_0:def 5;

        then 0 < ||.x.|| by CLVECT_1: 105;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    

     Lm2: for X be ComplexNormSpace, x,y be Point of X st for e be Real st e > 0 holds ||.(x - y).|| < e holds x = y

    proof

      let X be ComplexNormSpace;

      let x,y be Point of X;

      assume for e be Real st e > 0 holds ||.(x - y).|| < e;

      then (x - y) = ( 0. X) by Lm1;

      hence thesis by RLVECT_1: 21;

    end;

    

     Lm3: for X be ComplexNormSpace, x,y be Point of X, seq be Real_Sequence st (seq is convergent & ( lim seq) = 0 & for n be Nat holds ||.(x - y).|| <= (seq . n)) holds x = y

    proof

      let X be ComplexNormSpace;

      let x,y be Point of X;

      let seq be Real_Sequence such that

       A1: seq is convergent & ( lim seq) = 0 and

       A2: for n be Nat holds ||.(x - y).|| <= (seq . n);

      now

        let e be Real;

        assume 0 < e;

        then

        consider n be Nat such that

         A3: for m be Nat st n <= m holds |.((seq . m) - 0 ).| < e by A1, SEQ_2:def 7;

        

         A4: (seq . n) <= |.(seq . n).| by ABSVALUE: 4;

        

         A5: ||.(x - y).|| <= (seq . n) by A2;

         |.((seq . n) - 0 ).| < e by A3;

        then (seq . n) < e by A4, XXREAL_0: 2;

        hence ||.(x - y).|| < e by A5, XXREAL_0: 2;

      end;

      hence thesis by Lm2;

    end;

    theorem :: CLOPBAN3:42

    for X be Complex_Banach_Algebra, x be Point of X st ||.(( 1. X) - x).|| < 1 holds x is invertible & (x " ) = ( Sum ((( 1. X) - x) GeoSeq ))

    proof

      let X be Complex_Banach_Algebra;

      let x be Point of X such that

       A1: ||.(( 1. X) - x).|| < 1;

      set seq = ((( 1. X) - x) GeoSeq );

      

       A2: seq is summable by A1, Th40;

      then

       A3: ||.(seq ^\ 1).|| is convergent by CLOPBAN1: 40;

      reconsider y = ( Sum seq) as Element of X;

      

       A4: ( Partial_Sums seq) is convergent by A2;

      then ( lim ||.(( Partial_Sums seq) - y).||) = 0 by CLVECT_1: 118;

      

      then

       A5: ( lim ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||)) = ( ||.x.|| * 0 ) by A4, CLVECT_1: 118, SEQ_2: 8

      .= 0 ;

      ( lim (seq ^\ 1)) = ( 0. X) by A2, Th14;

      then

       A6: ( lim ||.(seq ^\ 1).||) = ||.( 0. X).|| by A2, CLOPBAN1: 40;

      

       A7: ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||) is convergent by A4, CLVECT_1: 118, SEQ_2: 7;

      then

       A8: ( ||.(seq ^\ 1).|| + ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||)) is convergent by A3, SEQ_2: 5;

      

       A9: ( lim ( ||.(seq ^\ 1).|| + ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||))) = (( lim ||.(seq ^\ 1).||) + ( lim ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||))) by A7, A3, SEQ_2: 6

      .= 0 by A5, A6;

      

       A10: for n be Nat holds ((( 1. X) - x) * (seq . n)) = (seq . (n + 1))

      proof

        defpred P[ Nat] means ((( 1. X) - x) * (seq . $1)) = (seq . ($1 + 1));

        

         A11: ((( 1. X) - x) * (seq . 0 )) = ((( 1. X) - x) * ( 1. X)) by Def4

        .= (( 1. X) - x) by VECTSP_1:def 4;

        

         A12: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A13: P[k];

          

          thus ((( 1. X) - x) * (seq . (k + 1))) = ((( 1. X) - x) * ((seq . k) * (( 1. X) - x))) by Def4

          .= (((( 1. X) - x) * (seq . k)) * (( 1. X) - x)) by GROUP_1:def 3

          .= (seq . ((k + 1) + 1)) by A13, Def4;

        end;

        (seq . ( 0 + 1)) = ((seq . 0 ) * (( 1. X) - x)) by Def4

        .= (( 1. X) * (( 1. X) - x)) by Def4

        .= (( 1. X) - x) by VECTSP_1:def 8;

        then

         A14: P[ 0 ] by A11;

        for n be Nat holds P[n] from NAT_1:sch 2( A14, A12);

        hence thesis;

      end;

      

       A15: for n be Nat holds ((( 1. X) - x) * (( Partial_Sums seq) . n)) = (((( Partial_Sums seq) ^\ 1) . n) - (seq . 0 ))

      proof

        defpred P[ Nat] means ((( 1. X) - x) * (( Partial_Sums seq) . $1)) = (((( Partial_Sums seq) ^\ 1) . $1) - (seq . 0 ));

        

         A16: ((( 1. X) - x) * (( Partial_Sums seq) . 0 )) = ((( 1. X) - x) * (seq . 0 )) by BHSP_4:def 1

        .= ((( 1. X) - x) * ( 1. X)) by Def4

        .= (( 1. X) - x) by VECTSP_1:def 4;

        

         A17: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A18: P[k];

          

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

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

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

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

          ((( 1. X) - x) * (( Partial_Sums seq) . (k + 1))) = ((( 1. X) - x) * ((( Partial_Sums seq) . k) + (seq . (k + 1)))) by BHSP_4:def 1

          .= (((( 1. X) - x) * (( Partial_Sums seq) . k)) + ((( 1. X) - x) * (seq . (k + 1)))) by VECTSP_1:def 2

          .= ((((( Partial_Sums seq) ^\ 1) . k) - (seq . 0 )) + (seq . ((k + 1) + 1))) by A10, A18;

          hence thesis by A19;

        end;

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

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

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

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

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

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

        .= ((seq . 0 ) * (( 1. X) - x)) by Def4

        .= (( 1. X) * (( 1. X) - x)) by Def4

        .= (( 1. X) - x) by VECTSP_1:def 8;

        then

         A20: P[ 0 ] by A16;

        for n be Nat holds P[n] from NAT_1:sch 2( A20, A17);

        hence thesis;

      end;

      now

        let n be Nat;

        reconsider yn = (( Partial_Sums seq) . n) as Element of X;

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

        then

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

        ((( 1. X) - (( 1. X) - x)) * yn) = ((( 1. X) * yn) - ((( 1. X) - x) * yn)) by Th38

        .= (yn - ((( 1. X) - x) * yn)) by VECTSP_1:def 8

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

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

        

        then ((( 1. X) - (( 1. X) - x)) * yn) = (((( Partial_Sums seq) . n) - ((( Partial_Sums seq) . n) + ((seq ^\ 1) . n))) + (seq . 0 )) by A21, NAT_1:def 3

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

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

        .= (( 0. X) - (((seq ^\ 1) . n) - (seq . 0 ))) by RLVECT_1: 29

        .= ( - (((seq ^\ 1) . n) - (seq . 0 ))) by RLVECT_1: 14

        .= ((seq . 0 ) - ((seq ^\ 1) . n)) by RLVECT_1: 33

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

        .= (( 1. X) - (seq . (n + 1))) by Def4;

        

        then

         A22: (( 1. X) - (x * yn)) = (( 1. X) - (( 1. X) - (seq . (n + 1)))) by Th38

        .= (seq . (n + 1)) by Th38

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

         ||.(x * (yn - y)).|| <= ( ||.x.|| * ||.(yn - y).||) by Th38;

        then

         A23: (( ||.(seq ^\ 1).|| . n) + ||.(x * (yn - y)).||) <= (( ||.(seq ^\ 1).|| . n) + ( ||.x.|| * ||.(yn - y).||)) by XREAL_1: 7;

         ||.(((seq ^\ 1) . n) + (x * (yn - y))).|| <= ( ||.((seq ^\ 1) . n).|| + ||.(x * (yn - y)).||) & ( ||.((seq ^\ 1) . n).|| + ||.(x * (yn - y)).||) = (( ||.(seq ^\ 1).|| . n) + ||.(x * (yn - y)).||) by CLVECT_1:def 13, NORMSP_0:def 4;

        then

         A24: ||.(((seq ^\ 1) . n) + (x * (yn - y))).|| <= (( ||.(seq ^\ 1).|| . n) + ( ||.x.|| * ||.(yn - y).||)) by A23, XXREAL_0: 2;

        (( 1. X) - (x * y)) = ((( 1. X) - ( 0. X)) - (x * y)) by RLVECT_1: 13

        .= ((( 1. X) - ((x * yn) - (x * yn))) - (x * y)) by RLVECT_1: 15

        .= (((( 1. X) - (x * yn)) + (x * yn)) - (x * y)) by RLVECT_1: 29

        .= ((( 1. X) - (x * yn)) + ((x * yn) - (x * y))) by RLVECT_1:def 3

        .= ((( 1. X) - (x * yn)) + (x * (yn - y))) by Th38;

        then ||.(( 1. X) - (x * y)).|| <= (( ||.(seq ^\ 1).|| . n) + ( ||.x.|| * ||.((( Partial_Sums seq) - y) . n).||)) by A22, A24, NORMSP_1:def 4;

        then ||.(( 1. X) - (x * y)).|| <= (( ||.(seq ^\ 1).|| . n) + ( ||.x.|| * ( ||.(( Partial_Sums seq) - y).|| . n))) by NORMSP_0:def 4;

        then ||.(( 1. X) - (x * y)).|| <= (( ||.(seq ^\ 1).|| . n) + (( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||) . n)) by SEQ_1: 9;

        hence ||.(( 1. X) - (x * y)).|| <= (( ||.(seq ^\ 1).|| + ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||)) . n) by SEQ_1: 7;

      end;

      then

       A25: ( 1. X) = (x * y) by A8, A9, Lm3;

      

       A26: for n be Nat holds ((( Partial_Sums seq) . n) * (( 1. X) - x)) = (((( Partial_Sums seq) ^\ 1) . n) - (seq . 0 ))

      proof

        defpred P[ Nat] means ((( Partial_Sums seq) . $1) * (( 1. X) - x)) = (((( Partial_Sums seq) ^\ 1) . $1) - (seq . 0 ));

        

         A27: ((( Partial_Sums seq) . 0 ) * (( 1. X) - x)) = ((seq . 0 ) * (( 1. X) - x)) by BHSP_4:def 1

        .= (( 1. X) * (( 1. X) - x)) by Def4

        .= (( 1. X) - x) by VECTSP_1:def 8;

        

         A28: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A29: P[k];

          

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

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

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

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

          ((( Partial_Sums seq) . (k + 1)) * (( 1. X) - x)) = (((( Partial_Sums seq) . k) + (seq . (k + 1))) * (( 1. X) - x)) by BHSP_4:def 1

          .= (((( Partial_Sums seq) . k) * (( 1. X) - x)) + ((seq . (k + 1)) * (( 1. X) - x))) by VECTSP_1:def 3

          .= ((((( Partial_Sums seq) ^\ 1) . k) - (seq . 0 )) + (seq . ((k + 1) + 1))) by A29, Def4;

          hence thesis by A30;

        end;

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

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

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

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

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

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

        .= ((seq . 0 ) * (( 1. X) - x)) by Def4

        .= (( 1. X) * (( 1. X) - x)) by Def4

        .= (( 1. X) - x) by VECTSP_1:def 8;

        then

         A31: P[ 0 ] by A27;

        for n be Nat holds P[n] from NAT_1:sch 2( A31, A28);

        hence thesis;

      end;

      now

        let n be Nat;

        reconsider yn = (( Partial_Sums seq) . n) as Element of X;

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

        then

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

        (yn * (( 1. X) - (( 1. X) - x))) = ((yn * ( 1. X)) - (yn * (( 1. X) - x))) by Th38

        .= (yn - (yn * (( 1. X) - x))) by VECTSP_1:def 4

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

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

        

        then (yn * (( 1. X) - (( 1. X) - x))) = (((( Partial_Sums seq) . n) - ((( Partial_Sums seq) . n) + ((seq ^\ 1) . n))) + (seq . 0 )) by A32, NAT_1:def 3

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

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

        .= (( 0. X) - (((seq ^\ 1) . n) - (seq . 0 ))) by RLVECT_1: 29

        .= ( - (((seq ^\ 1) . n) - (seq . 0 ))) by RLVECT_1: 14

        .= ((seq . 0 ) - ((seq ^\ 1) . n)) by RLVECT_1: 33

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

        .= (( 1. X) - (seq . (n + 1))) by Def4;

        

        then

         A33: (( 1. X) - (yn * x)) = (( 1. X) - (( 1. X) - (seq . (n + 1)))) by Th38

        .= (seq . (n + 1)) by Th38

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

         ||.((yn - y) * x).|| <= ( ||.(yn - y).|| * ||.x.||) by Th38;

        then

         A34: (( ||.(seq ^\ 1).|| . n) + ||.((yn - y) * x).||) <= (( ||.(seq ^\ 1).|| . n) + ( ||.(yn - y).|| * ||.x.||)) by XREAL_1: 7;

         ||.(((seq ^\ 1) . n) + ((yn - y) * x)).|| <= ( ||.((seq ^\ 1) . n).|| + ||.((yn - y) * x).||) & ( ||.((seq ^\ 1) . n).|| + ||.((yn - y) * x).||) = (( ||.(seq ^\ 1).|| . n) + ||.((yn - y) * x).||) by CLVECT_1:def 13, NORMSP_0:def 4;

        then

         A35: ||.(((seq ^\ 1) . n) + ((yn - y) * x)).|| <= (( ||.(seq ^\ 1).|| . n) + ( ||.(yn - y).|| * ||.x.||)) by A34, XXREAL_0: 2;

        (( 1. X) - (y * x)) = ((( 1. X) - ( 0. X)) - (y * x)) by RLVECT_1: 13

        .= ((( 1. X) - ((yn * x) - (yn * x))) - (y * x)) by RLVECT_1: 15

        .= (((( 1. X) - (yn * x)) + (yn * x)) - (y * x)) by RLVECT_1: 29

        .= ((( 1. X) - (yn * x)) + ((yn * x) - (y * x))) by RLVECT_1:def 3

        .= ((( 1. X) - (yn * x)) + ((yn - y) * x)) by Th38;

        then ||.(( 1. X) - (y * x)).|| <= (( ||.(seq ^\ 1).|| . n) + ( ||.((( Partial_Sums seq) - y) . n).|| * ||.x.||)) by A33, A35, NORMSP_1:def 4;

        then ||.(( 1. X) - (y * x)).|| <= (( ||.(seq ^\ 1).|| . n) + (( ||.(( Partial_Sums seq) - y).|| . n) * ||.x.||)) by NORMSP_0:def 4;

        then ||.(( 1. X) - (y * x)).|| <= (( ||.(seq ^\ 1).|| . n) + (( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||) . n)) by SEQ_1: 9;

        hence ||.(( 1. X) - (y * x)).|| <= (( ||.(seq ^\ 1).|| + ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||)) . n) by SEQ_1: 7;

      end;

      then

       A36: ( 1. X) = (y * x) by A8, A9, Lm3;

      hence x is invertible by A25, LOPBAN_3:def 4;

      hence thesis by A36, A25, LOPBAN_3:def 8;

    end;