lopban_3.miz



    begin

    theorem :: LOPBAN_3:1

    

     Th1: for X be add-associative right_zeroed right_complementable non empty NORMSTR 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 NORMSTR;

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

      let seq be sequence of X;

      :: LOPBAN_3:def1

      attr seq is summable means

      : Def1: ( Partial_Sums seq) is convergent;

    end

    registration

      let X be RealNormSpace;

      cluster summable for sequence of X;

      existence

      proof

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

        take C, ( 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 NORMSP_1: 6;

        hence thesis by A1;

      end;

    end

    definition

      let X be RealNormSpace;

      let seq be sequence of X;

      :: LOPBAN_3:def2

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

      correctness ;

    end

    definition

      let X be RealNormSpace;

      let seq be sequence of X;

      :: LOPBAN_3:def3

      attr seq is norm_summable means

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

    end

    theorem :: LOPBAN_3:2

    

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

    proof

      let X be RealNormSpace;

      let seq be sequence of X;

      let m be Nat;

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

      hence thesis;

    end;

    theorem :: LOPBAN_3:3

    

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

    proof

      let X be RealNormSpace;

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

    

     Th4: for X be RealNormSpace holds for 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 RealNormSpace;

      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, XREAL_1: 215;

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

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

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

        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 :: LOPBAN_3:5

    

     Th5: for X be RealNormSpace holds for 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 RealNormSpace;

      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;

          reconsider ss = s as Real;

          assume 0 < s;

          then

          consider k be Nat such that

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

          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 NORMSP_1: 7;

             ||.((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, NORMSP_1:def 1;

            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 RSSPACE3: 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, RSSPACE3: 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 :: LOPBAN_3:6

    

     Th6: for X be RealNormSpace 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

    proof

      let X be RealNormSpace;

      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)))

        .= ( ||.(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 :: LOPBAN_3:7

    

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

    proof

      let X be RealNormSpace;

      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 :: LOPBAN_3:8

    

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

    proof

      let X be RealNormSpace;

      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, NORMSP_1:def 7;

        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, NORMSP_1:def 7;

    end;

    theorem :: LOPBAN_3:9

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

    theorem :: LOPBAN_3:10

    

     Th10: for X be RealNormSpace holds for 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 RealNormSpace;

      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) + k) + ( - k)) by A7;

      then

      reconsider m1 = (m - k) as Nat;

      now

        assume not n1 <= m1;

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

        hence contradiction by A6;

      end;

      then (m1 + k) = m & ||.((seq . m1) - g1).|| < p by A5;

      hence thesis by A3, NAT_1:def 3;

    end;

    theorem :: LOPBAN_3:11

    

     Th11: for X be RealNormSpace holds for 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 RealNormSpace;

      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, NORMSP_1:def 7;

        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) + k) + ( - k)) by A7;

        then

        reconsider m1 = (m - k) as Nat;

        now

          assume not n1 <= m1;

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

          hence contradiction by A6;

        end;

        then (m1 + k) = m & ||.((seq . m1) - ( lim seq)).|| < p by A5;

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

      end;

      seq1 is convergent by A1, A2, Th10;

      hence thesis by A4, NORMSP_1:def 7;

    end;

    theorem :: LOPBAN_3:12

    

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

    proof

      let X be RealNormSpace;

      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 :: LOPBAN_3:13

    

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

    proof

      let X be RealNormSpace;

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

      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 :: LOPBAN_3:14

    

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

    proof

      let X be RealNormSpace;

      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, NORMSP_1: 26

      .= ( 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, NORMSP_1: 20;

      hence thesis by A3, A4, Th10, Th11;

    end;

    theorem :: LOPBAN_3:15

    

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

    proof

      let X be RealNormSpace;

      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 :: LOPBAN_3:16

    

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

    proof

      let X be RealNormSpace;

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

      let seq be norm_summable sequence of X;

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

      coherence by Def3;

    end

    registration

      let X be RealNormSpace;

      cluster summable -> convergent for sequence of X;

      coherence by Th14;

    end

    theorem :: LOPBAN_3:17

    

     Th17: for X be RealNormSpace holds for 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 RealNormSpace;

      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 NORMSP_1: 19;

      

       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, NORMSP_1: 25;

      hence thesis by A2, A3;

    end;

    theorem :: LOPBAN_3:18

    

     Th18: for X be RealNormSpace holds for 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 RealNormSpace;

      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 NORMSP_1: 20;

      

       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, NORMSP_1: 26;

      hence thesis by A2, A3;

    end;

    registration

      let X be RealNormSpace;

      let seq1,seq2 be summable sequence of X;

      cluster (seq1 + seq2) -> summable;

      coherence by Th17;

      cluster (seq1 - seq2) -> summable;

      coherence by Th18;

    end

    theorem :: LOPBAN_3:19

    

     Th19: for X be RealNormSpace holds for seq be sequence of X holds for z be Real holds ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq))

    proof

      let X be RealNormSpace;

      let seq be sequence of X;

      let z be Real;

      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, NORMSP_1:def 5

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

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

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

        .= ((z * ( Partial_Sums seq)) . (n + 1)) by NORMSP_1:def 5;

        hence P[(n + 1)];

      end;

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

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

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

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

      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 :: LOPBAN_3:20

    

     Th20: for X be RealNormSpace holds for seq be summable sequence of X holds for z be Real holds (z * seq) is summable & ( Sum (z * seq)) = (z * ( Sum seq))

    proof

      let X be RealNormSpace;

      let seq be summable sequence of X;

      let z be Real;

      

       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 NORMSP_1: 22;

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

      .= (z * ( Sum seq)) by A2, NORMSP_1: 28;

      hence thesis by A3, A1;

    end;

    registration

      let X be RealNormSpace;

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

      cluster (z * seq) -> summable;

      coherence by Th20;

    end

    theorem :: LOPBAN_3:21

    

     Th21: for X be RealNormSpace holds for 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 RealNormSpace;

      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 :: LOPBAN_3:22

    

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

    proof

      let X be RealNormSpace;

      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, NAT_1: 48, NORMSP_1: 20;

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

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

      cluster (seq ^\ n) -> summable;

      coherence by Th22;

    end

    theorem :: LOPBAN_3:23

    

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

    proof

      let X be RealNormSpace;

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

      let seq be norm_summable sequence of X;

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

      coherence by Th23;

    end

    theorem :: LOPBAN_3:24

    

     Th24: for X be RealBanachSpace holds for 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, LOPBAN_1:def 15, Th4;

    theorem :: LOPBAN_3:25

    

     Th25: for X be RealNormSpace holds for s be sequence of X holds for 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 RealNormSpace;

      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 ;

        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 NORMSP_1:def 1;

        (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 ||.((s1 . (n + (k + 1))) - (s1 . n)).|| <= ( ||.(s . ((n + k) + 1)).|| + ((s2 . (n + k)) - (s2 . n))) by A6, ABSVALUE:def 1;

        hence thesis by A4, ABSVALUE:def 1;

      end;

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

      .= 0 ;

      then

       A7: X[ 0 ] by COMPLEX1: 46;

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

      hence thesis by A1;

    end;

    theorem :: LOPBAN_3:26

    

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

    proof

      let X be RealBanachSpace;

      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;

        reconsider n as Nat;

        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 :: LOPBAN_3:27

    for X be RealNormSpace holds for rseq1 be Real_Sequence holds for 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 RealNormSpace;

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

      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 :: LOPBAN_3:28

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

    theorem :: LOPBAN_3:29

    for X be RealNormSpace holds for 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 :: LOPBAN_3:30

    for X be RealNormSpace holds for seq be sequence of X holds for 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 RealNormSpace;

      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 :: LOPBAN_3:31

    for X be RealNormSpace holds for seq be sequence of X holds for 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 RealNormSpace;

      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 :: LOPBAN_3:32

    for X be RealNormSpace holds for seq be sequence of X holds for 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 RealNormSpace;

      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 :: LOPBAN_3:33

    for X be RealNormSpace holds for seq be sequence of X holds for 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 RealNormSpace;

      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 :: LOPBAN_3:34

    for X be RealNormSpace holds for seq be sequence of X holds for 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 :: LOPBAN_3:35

    for X be RealNormSpace holds for seq be sequence of X holds for 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 :: LOPBAN_3:36

    for X be RealNormSpace holds for seq be sequence of X holds for 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 RealNormSpace;

      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 :: LOPBAN_3:37

    for X be RealNormSpace holds for 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 RealNormSpace;

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

      cluster norm_summable -> summable for sequence of X;

      coherence by Th26;

    end

    begin

    theorem :: LOPBAN_3:38

    

     Th38: for X be Banach_Algebra holds for x,y,z be Element of X holds for a,b be Real holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. X)) = x & (ex t be Element of X st (x + t) = ( 0. X)) & ((x * y) * z) = (x * (y * z)) & (1 * x) = x & ( 0 * x) = ( 0. X) & (a * ( 0. X)) = ( 0. X) & (( - 1) * x) = ( - x) & (x * ( 1. X)) = x & (( 1. X) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x)) & (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 & X is complete

    proof

      let X be Banach_Algebra;

      let x,y,z be Element of X;

      let a,b be Real;

      thus (x + y) = (y + x);

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

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

      thus ex t be Element of X st (x + t) = ( 0. X) by ALGSTR_0:def 11;

      thus ((x * y) * z) = (x * (y * z)) by GROUP_1:def 3;

      thus (1 * x) = x by RLVECT_1:def 8;

      thus ( 0 * x) = ( 0. X) by RLVECT_1: 10;

      thus (a * ( 0. X)) = ( 0. X) by RLVECT_1: 10;

      thus (( - 1) * x) = ( - x) by RLVECT_1: 16;

      thus (x * ( 1. X)) = x & (( 1. X) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x)) & (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 FUNCSDOM:def 9, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 2, VECTSP_1:def 3, VECTSP_1:def 4, VECTSP_1:def 8;

      

      thus ((a * b) * (x * y)) = (a * (b * (x * y))) by RLVECT_1:def 7

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

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

      thus (a * (x * y)) = (x * (a * y)) by LOPBAN_2: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 LOPBAN_2:def 9, NORMSP_0:def 5, NORMSP_1:def 1;

      thus thesis by LOPBAN_2:def 10;

    end;

    registration

      cluster -> well-unital for Banach_Algebra;

      coherence

      proof

        let X be Banach_Algebra;

        let x be Element of X;

        thus thesis by Th38;

      end;

    end

    definition

      let X be well-unital associative non empty multLoopStr;

      let v be Element of X;

      :: original: invertible

      redefine

      :: LOPBAN_3:def4

      attr v is invertible means ex w be Element of X st (v * w) = ( 1. X) & (w * v) = ( 1. X);

      compatibility

      proof

        thus v is invertible implies ex w be Element of X st (v * w) = ( 1. X) & (w * v) = ( 1. X)

        proof

          assume

           A1: v is invertible;

          then

          consider y be Element of X such that

           A2: (v * y) = ( 1. X) by ALGSTR_0:def 28;

          take y;

          thus (v * y) = ( 1. X) by A2;

          consider x be Element of X such that

           A3: (x * v) = ( 1. X) by A1, ALGSTR_0:def 27;

          x = (x * ( 1. X)) by VECTSP_1:def 6

          .= (( 1. X) * y) by A2, A3, GROUP_1:def 3

          .= y by VECTSP_1:def 6;

          hence thesis by A3;

        end;

        given w be Element of X such that

         A4: (v * w) = ( 1. X) & (w * v) = ( 1. X);

        thus v is right_invertible left_invertible by A4;

      end;

    end

    definition

      let X be non empty multMagma;

      let S be sequence of X;

      let a be Element of X;

      :: LOPBAN_3:def5

      func a * S -> sequence of X means for n be Nat holds (it . n) = (a * (S . n));

      existence

      proof

        deffunc F( Nat) = (a * (S . $1));

        consider S be sequence of X such that

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

        take S;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of X;

        assume that

         A2: for n be Nat holds (S1 . n) = (a * (S . n)) and

         A3: for n be Nat holds (S2 . n) = (a * (S . n));

        for n be Element of NAT holds (S1 . n) = (S2 . n)

        proof

          let n be Element of NAT ;

          (S1 . n) = (a * (S . n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: LOPBAN_3:def6

      func S * a -> sequence of X means for n be Nat holds (it . n) = ((S . n) * a);

      existence

      proof

        deffunc F( Nat) = ((S . $1) * a);

        consider S be sequence of X such that

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

        take S;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of X;

        assume that

         A5: for n be Nat holds (S1 . n) = ((S . n) * a) and

         A6: for n be Nat holds (S2 . n) = ((S . n) * a);

        for n be Element of NAT holds (S1 . n) = (S2 . n)

        proof

          let n be Element of NAT ;

          (S1 . n) = ((S . n) * a) by A5;

          hence thesis by A6;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let X be non empty multMagma;

      let seq1,seq2 be sequence of X;

      :: LOPBAN_3:def7

      func seq1 * seq2 -> sequence of X means for n be Nat holds (it . n) = ((seq1 . n) * (seq2 . n));

      existence

      proof

        deffunc F( Nat) = ((seq1 . $1) * (seq2 . $1));

        consider S be sequence of X such that

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

        take S;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of X;

        assume that

         A2: for n be Nat holds (S1 . n) = ((seq1 . n) * (seq2 . n)) and

         A3: for n be Nat holds (S2 . n) = ((seq1 . n) * (seq2 . n));

        for n be Element of NAT holds (S1 . n) = (S2 . n)

        proof

          let n be Element of NAT ;

          (S1 . n) = ((seq1 . n) * (seq2 . n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    notation

      let X be associative well-unital non empty multLoopStr;

      let x be Element of X;

      synonym x " for / x;

    end

    definition

      let X be associative well-unital non empty multLoopStr;

      let x be Element of X;

      :: original: "

      redefine

      :: LOPBAN_3:def8

      func x " means

      : Def8: (x * it ) = ( 1. X) & (it * x) = ( 1. X);

      compatibility

      proof

        let y be Element of X;

        consider x1 be Element of X such that

         A2: (x * x1) = ( 1. X) by A1;

        

         A3: x is right_mult-cancelable

        proof

          let y,z be Element of X;

          assume

           A4: (y * x) = (z * x);

          

          thus y = (y * ( 1. X)) by VECTSP_1:def 6

          .= ((z * x) * x1) by A2, A4, GROUP_1:def 3

          .= (z * ( 1. X)) by A2, GROUP_1:def 3

          .= z by VECTSP_1:def 6;

        end;

        thus y = (x " ) implies (x * y) = ( 1. X) & (y * x) = ( 1. X) by A1, A3, ALGSTR_0:def 30;

        thus thesis by A1, A3, ALGSTR_0:def 30;

      end;

    end

    definition

      let X be Banach_Algebra;

      let z be Element of X;

      :: LOPBAN_3:def9

      func z GeoSeq -> sequence of X means

      : Def9: (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 Banach_Algebra;

      let z be Element of X, n be Nat;

      :: LOPBAN_3:def10

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

      correctness ;

    end

    theorem :: LOPBAN_3:39

    for X be Banach_Algebra holds for z be Element of X holds (z #N 0 ) = ( 1. X) by Def9;

    theorem :: LOPBAN_3:40

    

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

    proof

      let X be Banach_Algebra;

      let z be Element of X;

      

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

        

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

        

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

        proof

          let k be Nat;

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

          then

           A4: ||.(((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 XREAL_1: 64;

          then

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

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

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

          hence thesis by A5, PREPOWER: 3;

        end;

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

        .= 1 by LOPBAN_2:def 10

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

        then

         A6: P[ 0 ] by A2;

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

        hence thesis;

      end;

      assume ||.z.|| < 1;

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

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

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

      then (z GeoSeq ) is norm_summable;

      hence thesis;

    end;

    theorem :: LOPBAN_3:41

    for X be Banach_Algebra holds for 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 RealNormSpace holds for x be Point of X st for e be Real st e > 0 holds ||.x.|| < e holds x = ( 0. X)

    proof

      let X be RealNormSpace;

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

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    

     Lm2: for X be RealNormSpace holds for 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 RealNormSpace;

      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 RealNormSpace holds for x,y be Point of X holds for 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 RealNormSpace;

      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 :: LOPBAN_3:42

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

    proof

      let X be 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 LOPBAN_1: 41;

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

      

       A4: ( Partial_Sums seq) is convergent by A2;

      then ( lim ||.(( Partial_Sums seq) - y).||) = 0 by NORMSP_1: 24;

      

      then

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

      .= 0 ;

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

      then

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

      

       A7: ( ||.x.|| (#) ||.(( Partial_Sums seq) - y).||) is convergent by A4, NORMSP_1: 24, 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 Def9

        .= (( 1. X) - x) by Th38;

        

         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 Def9

          .= (((( 1. X) - x) * (seq . k)) * (( 1. X) - x)) by Th38

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

        end;

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

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

        .= (( 1. X) - x) by Th38;

        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 Def9

        .= (( 1. X) - x) by Th38;

        

         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 Th38

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

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

        .= (( 1. X) - x) by Th38;

        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 Th38

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

        

        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 NORMSP_0:def 4, NORMSP_1:def 1;

        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 Def9

        .= (( 1. X) - x) by Th38;

        

         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 Th38

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

          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 Def9

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

        .= (( 1. X) - x) by Th38;

        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 Th38

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

        

        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 NORMSP_0:def 4, NORMSP_1:def 1;

        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;

      hence thesis by A36, A25, Def8;

    end;