lopban_4.miz



    begin

    reserve X for Banach_Algebra,

w,z,z1,z2 for Element of X,

k,l,m,n,n1,n2 for Nat,

seq,seq1,seq2,s,s9 for sequence of X,

rseq for Real_Sequence;

    definition

      let X be non empty multMagma;

      let x,y be Element of X;

      :: LOPBAN_4:def1

      pred x,y are_commutative means (x * y) = (y * x);

      reflexivity ;

      symmetry ;

    end

    

     Lm1: (z * (z #N n)) = (z #N (n + 1)) & ((z #N n) * z) = (z #N (n + 1)) & (z * (z #N n)) = ((z #N n) * z)

    proof

      defpred P[ Nat] means (z * (z #N $1)) = (z #N ($1 + 1));

      

       A1: (z #N ( 0 + 1)) = (((z GeoSeq ) . 0 ) * z) by LOPBAN_3:def 9

      .= (( 1. X) * z) by LOPBAN_3:def 9

      .= z by LOPBAN_3: 38;

      

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

      proof

        let k be Nat such that

         A3: P[k];

        

        thus (z * (z #N (k + 1))) = (z * (((z GeoSeq ) . k) * z)) by LOPBAN_3:def 9

        .= ((z * (z #N k)) * z) by LOPBAN_3: 38

        .= (z #N ((k + 1) + 1)) by A3, LOPBAN_3:def 9;

      end;

      (z * (z #N 0 )) = (z * ( 1. X)) by LOPBAN_3:def 9

      .= z by LOPBAN_3: 38;

      then

       A4: P[ 0 ] by A1;

      

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

      now

        let n;

        thus (z * (z #N n)) = (z #N (n + 1)) by A5;

        thus ((z #N n) * z) = (z #N (n + 1)) by LOPBAN_3:def 9;

        hence (z * (z #N n)) = ((z #N n) * z) by A5;

      end;

      hence thesis;

    end;

    

     Lm2: for z, w st (z,w) are_commutative holds (w * (z #N n)) = ((z #N n) * w) & (z * (w #N n)) = ((w #N n) * z)

    proof

      let z, w such that

       A1: (z,w) are_commutative ;

      defpred P[ Nat] means (w * (z #N $1)) = ((z #N $1) * w) & (z * (w #N $1)) = ((w #N $1) * z);

      

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

      proof

        let k be Nat such that

         A3: P[k];

        

         A4: (z * (w #N (k + 1))) = (z * ((w #N k) * w)) by Lm1

        .= ((z * (w #N k)) * w) by LOPBAN_3: 38

        .= ((w #N k) * (z * w)) by A3, LOPBAN_3: 38

        .= ((w #N k) * (w * z)) by A1

        .= (((w #N k) * w) * z) by LOPBAN_3: 38

        .= ((w #N (k + 1)) * z) by Lm1;

        (w * (z #N (k + 1))) = (w * ((z #N k) * z)) by Lm1

        .= ((w * (z #N k)) * z) by LOPBAN_3: 38

        .= ((z #N k) * (w * z)) by A3, LOPBAN_3: 38

        .= ((z #N k) * (z * w)) by A1

        .= (((z #N k) * z) * w) by LOPBAN_3: 38

        .= ((z #N (k + 1)) * w) by Lm1;

        hence thesis by A4;

      end;

      

       A5: (w #N 0 ) = ( 1. X) by LOPBAN_3:def 9;

      

      then

       A6: (z * (w #N 0 )) = z by LOPBAN_3: 38

      .= ((w #N 0 ) * z) by A5, LOPBAN_3: 38;

      

       A7: (z #N 0 ) = ( 1. X) by LOPBAN_3:def 9;

      

      then (w * (z #N 0 )) = w by LOPBAN_3: 38

      .= ((z #N 0 ) * w) by A7, LOPBAN_3: 38;

      then

       A8: P[ 0 ] by A6;

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

      hence thesis;

    end;

    theorem :: LOPBAN_4:1

    

     Th1: seq1 is convergent & seq2 is convergent & ( lim (seq1 - seq2)) = ( 0. X) implies ( lim seq1) = ( lim seq2)

    proof

      assume that

       A1: seq1 is convergent and

       A2: seq2 is convergent and

       A3: ( lim (seq1 - seq2)) = ( 0. X);

      (( lim seq1) - ( lim seq2)) = ( 0. X) by A1, A2, A3, NORMSP_1: 26;

      then ((( lim seq1) - ( lim seq2)) + ( lim seq2)) = ( lim seq2) by LOPBAN_3: 38;

      then (( lim seq1) - (( lim seq2) - ( lim seq2))) = ( lim seq2) by LOPBAN_3: 38;

      then (( lim seq1) - ( 0. X)) = ( lim seq2) by RLVECT_1: 15;

      hence thesis by RLVECT_1: 13;

    end;

    theorem :: LOPBAN_4:2

    

     Th2: for z st for n be Nat holds (s . n) = z holds ( lim s) = z

    proof

      let z;

      assume

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

       A2:

      now

        let p be Real such that

         A3: 0 < p;

        reconsider k = 0 as Nat;

        take k;

        let n such that k <= n;

        (s . n) = z by A1;

        hence ||.((s . n) - z).|| < p by A3, NORMSP_1: 6;

      end;

      then s is convergent;

      hence thesis by A2, NORMSP_1:def 7;

    end;

    theorem :: LOPBAN_4:3

    

     Th3: s is convergent & s9 is convergent implies (s * s9) is convergent

    proof

      assume that

       A1: s is convergent and

       A2: s9 is convergent;

      consider g1 be Point of X such that

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

       ||.s.|| is bounded by A1, NORMSP_1: 23, SEQ_2: 13;

      then

      consider R be Real such that

       A4: for n be Nat holds ( ||.s.|| . n) < R by SEQ_2:def 3;

       A5:

      now

        let n;

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

        hence ||.(s . n).|| < R by A4;

      end;

       ||.(s . 1).|| = ( ||.s.|| . 1) by NORMSP_0:def 4;

      then 0 <= ( ||.s.|| . 1) by NORMSP_1: 4;

      then

       A6: 0 < R by A4;

      consider g2 be Point of X such that

       A7: for p be Real st 0 < p holds ex n st for m st n <= m holds ||.((s9 . m) - g2).|| < p by A2;

      take g = (g1 * g2);

      let p be Real;

      reconsider R as Real;

      

       A8: ( 0 + 0 ) < ( ||.g2.|| + R) by A6, NORMSP_1: 4, XREAL_1: 8;

      assume

       A9: 0 < p;

      then

      consider n1 such that

       A10: for m st n1 <= m holds ||.((s . m) - g1).|| < (p / ( ||.g2.|| + R)) by A3, A8, XREAL_1: 139;

      consider n2 such that

       A11: for m st n2 <= m holds ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A7, A8, A9, XREAL_1: 139;

      take n = (n1 + n2);

      let m such that

       A12: n <= m;

      n2 <= n by NAT_1: 12;

      then n2 <= m by A12, XXREAL_0: 2;

      then

       A13: ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A11;

      

       A14: 0 <= ||.(s . m).|| by NORMSP_1: 4;

      

       A15: ||.((s . m) * ((s9 . m) - g2)).|| <= ( ||.(s . m).|| * ||.((s9 . m) - g2).||) by LOPBAN_3: 38;

      

       A16: 0 <= ||.((s9 . m) - g2).|| by NORMSP_1: 4;

      n1 <= (n1 + n2) by NAT_1: 12;

      then n1 <= m by A12, XXREAL_0: 2;

      then

       A17: ||.((s . m) - g1).|| <= (p / ( ||.g2.|| + R)) by A10;

       ||.(((s * s9) . m) - g).|| = ||.(((s . m) * (s9 . m)) - (g1 * g2)).|| by LOPBAN_3:def 7

      .= ||.((((s . m) * (s9 . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by LOPBAN_3: 38

      .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by LOPBAN_3: 38

      .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).|| by LOPBAN_3: 38;

      then

       A18: ||.(((s * s9) . m) - g).|| <= ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) by NORMSP_1:def 1;

       ||.(s . m).|| < R by A5;

      then ( ||.(s . m).|| * ||.((s9 . m) - g2).||) < (R * (p / ( ||.g2.|| + R))) by A14, A16, A13, XREAL_1: 96;

      then

       A19: ||.((s . m) * ((s9 . m) - g2)).|| < (R * (p / ( ||.g2.|| + R))) by A15, XXREAL_0: 2;

      

       A20: ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * ||.((s . m) - g1).||) by LOPBAN_3: 38;

       0 <= ||.g2.|| by NORMSP_1: 4;

      then ( ||.g2.|| * ||.((s . m) - g1).||) <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A17, XREAL_1: 64;

      then

       A21: ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A20, XXREAL_0: 2;

      ((R * (p / ( ||.g2.|| + R))) + ( ||.g2.|| * (p / ( ||.g2.|| + R)))) = ((p / ( ||.g2.|| + R)) * ( ||.g2.|| + R))

      .= p by A8, XCMPLX_1: 87;

      then ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) < p by A19, A21, XREAL_1: 8;

      hence ||.(((s * s9) . m) - g).|| < p by A18, XXREAL_0: 2;

    end;

    theorem :: LOPBAN_4:4

    

     Th4: s is convergent implies (z * s) is convergent

    proof

      

       A1: 0 <= ||.z.|| by NORMSP_1: 4;

      assume s is convergent;

      then

      consider g1 be Point of X such that

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

      take g = (z * g1);

      let p be Real;

      

       A3: ( 0 + 0 ) < ( ||.z.|| + 1) by NORMSP_1: 4, XREAL_1: 8;

      assume

       A4: 0 < p;

      then

      consider n such that

       A5: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A2, A3, XREAL_1: 139;

      take n;

      let m;

      assume n <= m;

      then

       A6: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A5;

      

       A7: ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * ||.((s . m) - g1).||) by LOPBAN_3: 38;

      

       A8: ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

       0 < (p / ( ||.z.|| + 1)) by A3, A4, XREAL_1: 139;

      then

       A9: ( ||.z.|| * (p / ( ||.z.|| + 1))) < (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) by A1, A8, XREAL_1: 97;

      

       A10: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by LOPBAN_3:def 5

      .= ||.(z * ((s . m) - g1)).|| by LOPBAN_3: 38;

       0 <= ||.((s . m) - g1).|| by NORMSP_1: 4;

      then ( ||.z.|| * ||.((s . m) - g1).||) <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A1, A6, XREAL_1: 66;

      then

       A11: ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A7, XXREAL_0: 2;

      (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) = p by A3, XCMPLX_1: 87;

      hence ||.(((z * s) . m) - g).|| < p by A10, A11, A9, XXREAL_0: 2;

    end;

    theorem :: LOPBAN_4:5

    

     Th5: s is convergent implies (s * z) is convergent

    proof

      

       A1: 0 <= ||.z.|| by NORMSP_1: 4;

      assume s is convergent;

      then

      consider g1 be Point of X such that

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

      take g = (g1 * z);

      let p be Real;

      

       A3: ( 0 + 0 ) < ( ||.z.|| + 1) by NORMSP_1: 4, XREAL_1: 8;

      assume

       A4: 0 < p;

      then

      consider n such that

       A5: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A2, A3, XREAL_1: 139;

      take n;

      let m;

      assume n <= m;

      then

       A6: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A5;

      

       A7: ||.(((s . m) - g1) * z).|| <= ( ||.((s . m) - g1).|| * ||.z.||) by LOPBAN_3: 38;

      

       A8: ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

       0 < (p / ( ||.z.|| + 1)) by A3, A4, XREAL_1: 139;

      then

       A9: ((p / ( ||.z.|| + 1)) * ||.z.||) < ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) by A1, A8, XREAL_1: 97;

      

       A10: ||.(((s * z) . m) - g).|| = ||.(((s . m) * z) - (g1 * z)).|| by LOPBAN_3:def 6

      .= ||.(((s . m) - g1) * z).|| by LOPBAN_3: 38;

       0 <= ||.((s . m) - g1).|| by NORMSP_1: 4;

      then ( ||.((s . m) - g1).|| * ||.z.||) <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A1, A6, XREAL_1: 66;

      then

       A11: ||.(((s . m) - g1) * z).|| <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A7, XXREAL_0: 2;

      ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) = p by A3, XCMPLX_1: 87;

      hence ||.(((s * z) . m) - g).|| < p by A10, A11, A9, XXREAL_0: 2;

    end;

    theorem :: LOPBAN_4:6

    

     Th6: s is convergent implies ( lim (z * s)) = (z * ( lim s))

    proof

      assume

       A1: s is convergent;

      set g1 = ( lim s);

      set g = (z * g1);

      

       A2: ( 0 + 0 ) < ( ||.z.|| + 1) by NORMSP_1: 4, XREAL_1: 8;

      

       A3: 0 <= ||.z.|| by NORMSP_1: 4;

       A4:

      now

        let p be Real;

        assume 0 < p;

        then

         A5: 0 < (p / ( ||.z.|| + 1)) by A2, XREAL_1: 139;

        then

        consider n such that

         A6: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A1, NORMSP_1:def 7;

        take n;

        let m;

        assume n <= m;

        then

         A7: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A6;

         0 <= ||.((s . m) - g1).|| by NORMSP_1: 4;

        then

         A8: ( ||.z.|| * ||.((s . m) - g1).||) <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A3, A7, XREAL_1: 66;

         ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * ||.((s . m) - g1).||) by LOPBAN_3: 38;

        then

         A9: ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A8, XXREAL_0: 2;

        

         A10: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by LOPBAN_3:def 5

        .= ||.(z * ((s . m) - g1)).|| by LOPBAN_3: 38;

        ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

        then

         A11: ( ||.z.|| * (p / ( ||.z.|| + 1))) < (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) by A3, A5, XREAL_1: 97;

        (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) = p by A2, XCMPLX_1: 87;

        hence ||.(((z * s) . m) - g).|| < p by A10, A9, A11, XXREAL_0: 2;

      end;

      (z * s) is convergent by A1, Th4;

      hence thesis by A4, NORMSP_1:def 7;

    end;

    theorem :: LOPBAN_4:7

    

     Th7: s is convergent implies ( lim (s * z)) = (( lim s) * z)

    proof

      assume

       A1: s is convergent;

      set g1 = ( lim s);

      set g = (g1 * z);

      

       A2: ( 0 + 0 ) < ( ||.z.|| + 1) by NORMSP_1: 4, XREAL_1: 8;

      

       A3: 0 <= ||.z.|| by NORMSP_1: 4;

       A4:

      now

        let p be Real;

        assume 0 < p;

        then

         A5: 0 < (p / ( ||.z.|| + 1)) by A2, XREAL_1: 139;

        then

        consider n such that

         A6: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A1, NORMSP_1:def 7;

        take n;

        let m;

        assume n <= m;

        then

         A7: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A6;

         0 <= ||.((s . m) - g1).|| by NORMSP_1: 4;

        then

         A8: ( ||.((s . m) - g1).|| * ||.z.||) <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A3, A7, XREAL_1: 66;

         ||.(((s . m) - g1) * z).|| <= ( ||.((s . m) - g1).|| * ||.z.||) by LOPBAN_3: 38;

        then

         A9: ||.(((s . m) - g1) * z).|| <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A8, XXREAL_0: 2;

        

         A10: ||.(((s * z) . m) - g).|| = ||.(((s . m) * z) - (g1 * z)).|| by LOPBAN_3:def 6

        .= ||.(((s . m) - g1) * z).|| by LOPBAN_3: 38;

        ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

        then

         A11: ((p / ( ||.z.|| + 1)) * ||.z.||) < ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) by A3, A5, XREAL_1: 97;

        ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) = p by A2, XCMPLX_1: 87;

        hence ||.(((s * z) . m) - g).|| < p by A10, A9, A11, XXREAL_0: 2;

      end;

      (s * z) is convergent by A1, Th5;

      hence thesis by A4, NORMSP_1:def 7;

    end;

    theorem :: LOPBAN_4:8

    

     Th8: s is convergent & s9 is convergent implies ( lim (s * s9)) = (( lim s) * ( lim s9))

    proof

      assume that

       A1: s is convergent and

       A2: s9 is convergent;

       ||.s.|| is bounded by A1, NORMSP_1: 23, SEQ_2: 13;

      then

      consider R be Real such that

       A3: for n be Nat holds ( ||.s.|| . n) < R by SEQ_2:def 3;

      set g2 = ( lim s9);

      set g1 = ( lim s);

      set g = (g1 * g2);

       A4:

      now

        let n;

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

        hence ||.(s . n).|| < R by A3;

      end;

       ||.(s . 1).|| = ( ||.s.|| . 1) by NORMSP_0:def 4;

      then 0 <= ( ||.s.|| . 1) by NORMSP_1: 4;

      then

       A5: 0 < R by A3;

      reconsider R as Real;

      

       A6: ( 0 + 0 ) < ( ||.g2.|| + R) by A5, NORMSP_1: 4, XREAL_1: 8;

      

       A7: 0 <= ||.g2.|| by NORMSP_1: 4;

       A8:

      now

        let p be Real;

        assume 0 < p;

        then

         A9: 0 < (p / ( ||.g2.|| + R)) by A6, XREAL_1: 139;

        then

        consider n1 such that

         A10: for m st n1 <= m holds ||.((s . m) - g1).|| < (p / ( ||.g2.|| + R)) by A1, NORMSP_1:def 7;

        consider n2 such that

         A11: for m st n2 <= m holds ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A2, A9, NORMSP_1:def 7;

        take n = (n1 + n2);

        let m such that

         A12: n <= m;

        n1 <= (n1 + n2) by NAT_1: 12;

        then n1 <= m by A12, XXREAL_0: 2;

        then ||.((s . m) - g1).|| <= (p / ( ||.g2.|| + R)) by A10;

        then

         A13: ( ||.g2.|| * ||.((s . m) - g1).||) <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A7, XREAL_1: 64;

         ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * ||.((s . m) - g1).||) by LOPBAN_3: 38;

        then

         A14: ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A13, XXREAL_0: 2;

        

         A15: 0 <= ||.(s . m).|| by NORMSP_1: 4;

         ||.(((s * s9) . m) - g).|| = ||.(((s . m) * (s9 . m)) - (g1 * g2)).|| by LOPBAN_3:def 7

        .= ||.((((s . m) * (s9 . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by LOPBAN_3: 38

        .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by LOPBAN_3: 38

        .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).|| by LOPBAN_3: 38;

        then

         A16: ||.(((s * s9) . m) - g).|| <= ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) by NORMSP_1:def 1;

        

         A17: ||.((s . m) * ((s9 . m) - g2)).|| <= ( ||.(s . m).|| * ||.((s9 . m) - g2).||) by LOPBAN_3: 38;

        n2 <= n by NAT_1: 12;

        then n2 <= m by A12, XXREAL_0: 2;

        then

         A18: ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A11;

        

         A19: 0 <= ||.((s9 . m) - g2).|| by NORMSP_1: 4;

         ||.(s . m).|| < R by A4;

        then ( ||.(s . m).|| * ||.((s9 . m) - g2).||) < (R * (p / ( ||.g2.|| + R))) by A15, A19, A18, XREAL_1: 96;

        then

         A20: ||.((s . m) * ((s9 . m) - g2)).|| < (R * (p / ( ||.g2.|| + R))) by A17, XXREAL_0: 2;

        ((R * (p / ( ||.g2.|| + R))) + ( ||.g2.|| * (p / ( ||.g2.|| + R)))) = ((p / ( ||.g2.|| + R)) * ( ||.g2.|| + R))

        .= p by A6, XCMPLX_1: 87;

        then ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) < p by A20, A14, XREAL_1: 8;

        hence ||.(((s * s9) . m) - g).|| < p by A16, XXREAL_0: 2;

      end;

      (s * s9) is convergent by A1, A2, Th3;

      hence thesis by A8, NORMSP_1:def 7;

    end;

    theorem :: LOPBAN_4:9

    

     Th9: ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq)) & ( Partial_Sums (seq * z)) = (( Partial_Sums seq) * z)

    proof

      

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

      proof

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

         A2:

        now

          let n;

          assume

           A3: P[n];

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

          .= (((( Partial_Sums seq) . n) * z) + ((seq * z) . (n + 1))) by A3, LOPBAN_3:def 6

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

          .= (((( Partial_Sums seq) . n) + (seq . (n + 1))) * z) by LOPBAN_3: 38

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

          .= ((( Partial_Sums seq) * z) . (n + 1)) by LOPBAN_3:def 6;

          hence P[(n + 1)];

        end;

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

        .= ((seq . 0 ) * z) by LOPBAN_3:def 6

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

        .= ((( Partial_Sums seq) * z) . 0 ) by LOPBAN_3:def 6;

        then

         A4: P[ 0 ];

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

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

        hence thesis by FUNCT_2: 63;

      end;

      ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq))

      proof

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

         A5:

        now

          let n;

          assume

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

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

          .= (z * ((( Partial_Sums seq) . n) + (seq . (n + 1)))) by LOPBAN_3: 38

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

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

          hence P[(n + 1)];

        end;

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

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

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

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

        then

         A7: P[ 0 ];

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

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

        hence thesis by FUNCT_2: 63;

      end;

      hence thesis by A1;

    end;

    theorem :: LOPBAN_4:10

    

     Th10: ||.(( Partial_Sums seq) . k).|| <= (( Partial_Sums ||.seq.||) . k)

    proof

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

       A1:

      now

        let k;

        assume P[k];

        then

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

        

         A3: ||.((( Partial_Sums seq) . k) + (seq . (k + 1))).|| <= ( ||.(( Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).||) by NORMSP_1:def 1;

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

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

        then ||.(( Partial_Sums seq) . (k + 1)).|| <= ((( Partial_Sums ||.seq.||) . k) + ( ||.seq.|| . (k + 1))) by NORMSP_0:def 4;

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

      end;

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

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

      then

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

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

      hence thesis;

    end;

    theorem :: LOPBAN_4:11

    

     Th11: (for n st n <= m holds (seq1 . n) = (seq2 . n)) implies (( Partial_Sums seq1) . m) = (( Partial_Sums seq2) . m)

    proof

      defpred P[ Nat] means $1 <= m implies (( Partial_Sums seq1) . $1) = (( Partial_Sums seq2) . $1);

      assume

       A1: for n st n <= m holds (seq1 . n) = (seq2 . n);

      

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

      proof

        let k be Nat such that

         A3: P[k];

        assume

         A4: (k + 1) <= m;

        k < (k + 1) by XREAL_1: 29;

        

        hence (( Partial_Sums seq1) . (k + 1)) = ((( Partial_Sums seq2) . k) + (seq1 . (k + 1))) by A3, A4, BHSP_4:def 1, XXREAL_0: 2

        .= ((( Partial_Sums seq2) . k) + (seq2 . (k + 1))) by A1, A4

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

      end;

      

       A5: P[ 0 ]

      proof

        assume 0 <= m;

        

        thus (( Partial_Sums seq1) . 0 ) = (seq1 . 0 ) by BHSP_4:def 1

        .= (seq2 . 0 ) by A1

        .= (( Partial_Sums seq2) . 0 ) by BHSP_4:def 1;

      end;

      for k holds P[k] from NAT_1:sch 2( A5, A2);

      hence thesis;

    end;

    theorem :: LOPBAN_4:12

    

     Th12: (for n holds ||.(seq . n).|| <= (rseq . n)) & rseq is convergent & ( lim rseq) = 0 implies seq is convergent & ( lim seq) = ( 0. X)

    proof

      assume that

       A1: for n holds ||.(seq . n).|| <= (rseq . n) and

       A2: rseq is convergent and

       A3: ( lim rseq) = 0 ;

      now

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         A4: for m be Nat st n <= m holds |.((rseq . m) - 0 ).| < p by A2, A3, SEQ_2:def 7;

        reconsider n as Nat;

        take n;

        let m;

        assume n <= m;

        then

         A5: |.((rseq . m) - 0 ).| < p by A4;

        

         A6: ||.((seq . m) - ( 0. X)).|| = ||.(seq . m).|| by RLVECT_1: 13;

        

         A7: (rseq . m) <= |.(rseq . m).| by ABSVALUE: 4;

         ||.(seq . m).|| <= (rseq . m) by A1;

        then ||.((seq . m) - ( 0. X)).|| <= |.(rseq . m).| by A6, A7, XXREAL_0: 2;

        hence ||.((seq . m) - ( 0. X)).|| < p by A5, XXREAL_0: 2;

      end;

      then

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

      hence seq is convergent;

      hence thesis by A8, NORMSP_1:def 7;

    end;

    definition

      let X;

      let z be Element of X;

      :: LOPBAN_4:def2

      func z rExpSeq -> sequence of X means

      : Def2: for n holds (it . n) = ((1 / (n ! )) * (z #N n));

      existence

      proof

        deffunc U( Nat) = ((1 / ($1 ! )) * (z #N $1));

        consider s be sequence of X such that

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

        take s;

        let n;

        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) = ((1 / (n ! )) * (z #N n)) and

         A3: for n be Nat holds (S2 . n) = ((1 / (n ! )) * (z #N n));

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

        proof

          let n be Element of NAT ;

          (S1 . n) = ((1 / (n ! )) * (z #N n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    scheme :: LOPBAN_4:sch1

    ExNormSpaceCASE { RNS() -> non empty Banach_Algebra , F( Nat, Nat) -> Point of RNS() } :

for k holds ex seq be sequence of RNS() st for n holds (n <= k implies (seq . n) = F(k,n)) & (n > k implies (seq . n) = ( 0. RNS()));

      let k;

      defpred P[ object, object] means ex n st (n = $1 & (n <= k implies $2 = F(k,n)) & (n > k implies $2 = ( 0. RNS())));

       A1:

      now

        let x be object;

        assume x in NAT ;

        then

        consider n such that

         A2: n = x;

        reconsider chk = ( CHK (n,k)) as Element of REAL by XREAL_0:def 1;

        

         A3: n > k implies (chk * F(k,n)) = ( 0. RNS()) by RLVECT_1: 10, SIN_COS:def 1;

        reconsider y = (chk * F(k,n)) as object;

        take y;

        now

          assume n <= k;

          

          hence (chk * F(k,n)) = (1 * F(k,n)) by SIN_COS:def 1

          .= F(k,n) by RLVECT_1:def 8;

        end;

        hence P[x, y] by A2, A3;

      end;

      consider f be Function such that

       A4: ( dom f) = NAT and

       A5: for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A1);

      now

        let x be object;

        assume x in NAT ;

        then ex n st n = x & (n <= k implies (f . x) = F(k,n)) & (n > k implies (f . x) = ( 0. RNS())) by A5;

        hence (f . x) in the carrier of RNS();

      end;

      then

      reconsider f as sequence of RNS() by A4, FUNCT_2: 3;

      take seq = f;

      let n;

      

       A6: n in NAT by ORDINAL1:def 12;

      ex l be Nat st l = n & (l <= k implies (seq . n) = F(k,l)) & (l > k implies (seq . n) = ( 0. RNS())) by A5, A6;

      hence thesis;

    end;

    theorem :: LOPBAN_4:13

    

     Th13: (for k st 0 < k holds (((k -' 1) ! ) * k) = (k ! )) & for m, k st k <= m holds (((m -' k) ! ) * ((m + 1) - k)) = (((m + 1) -' k) ! )

    proof

       A1:

      now

        let k;

        

         A2: k in NAT by ORDINAL1:def 12;

        assume 0 < k;

        then ( 0 + 1) <= k by INT_1: 7, A2;

        

        then ((k -' 1) + 1) = ((k - 1) + 1) by XREAL_1: 233

        .= k;

        hence (k ! ) = (((k -' 1) ! ) * k) by NEWTON: 15;

      end;

      now

        let m, k such that

         A3: k <= m;

        m <= (m + 1) by XREAL_1: 29;

        

        then ((m + 1) -' k) = ((m + 1) - k) by A3, XREAL_1: 233, XXREAL_0: 2

        .= ((m - k) + 1)

        .= ((m -' k) + 1) by A3, XREAL_1: 233;

        

        hence (((m + 1) -' k) ! ) = (((m -' k) ! ) * ((m -' k) + 1)) by NEWTON: 15

        .= (((m -' k) ! ) * ((m - k) + 1)) by A3, XREAL_1: 233

        .= (((m -' k) ! ) * ((m + 1) - k));

      end;

      hence thesis by A1;

    end;

    definition

      let n be Nat;

      :: LOPBAN_4:def3

      func Coef (n) -> Real_Sequence means

      : Def3: for k be Nat holds (k <= n implies (it . k) = ((n ! ) / ((k ! ) * ((n -' k) ! )))) & (k > n implies (it . k) = 0 );

      existence

      proof

        deffunc U( Nat, Nat) = (($1 ! ) / (($2 ! ) * (($1 -' $2) ! )));

        for n be Nat holds ex seq be Real_Sequence st for k be Nat holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from SIN_COS:sch 2;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Real_Sequence;

        assume that

         A1: for k be Nat holds (k <= n implies (seq1 . k) = ((n ! ) / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq1 . k) = 0 ) and

         A2: for k be Nat holds (k <= n implies (seq2 . k) = ((n ! ) / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq2 . k) = 0 );

        now

          let k be Element of NAT ;

          per cases ;

            suppose

             A3: k <= n;

            

            hence (seq1 . k) = ((n ! ) / ((k ! ) * ((n -' k) ! ))) by A1

            .= (seq2 . k) by A2, A3;

          end;

            suppose

             A4: k > n;

            

            hence (seq1 . k) = 0 by A1

            .= (seq2 . k) by A2, A4;

          end;

        end;

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let n be Nat;

      :: LOPBAN_4:def4

      func Coef_e (n) -> Real_Sequence means

      : Def4: for k be Nat holds (k <= n implies (it . k) = (1 / ((k ! ) * ((n -' k) ! )))) & (k > n implies (it . k) = 0 );

      existence

      proof

        deffunc U( Nat, Nat) = (1 / (($2 ! ) * (($1 -' $2) ! )));

        for n be Nat holds ex seq be Real_Sequence st for k be Nat holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from SIN_COS:sch 2;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Real_Sequence;

        assume that

         A1: for k be Nat holds (k <= n implies (seq1 . k) = (1 / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq1 . k) = 0 ) and

         A2: for k be Nat holds (k <= n implies (seq2 . k) = (1 / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq2 . k) = 0 );

        now

          let k be Element of NAT ;

          per cases ;

            suppose

             A3: k <= n;

            

            hence (seq1 . k) = (1 / ((k ! ) * ((n -' k) ! ))) by A1

            .= (seq2 . k) by A2, A3;

          end;

            suppose

             A4: k > n;

            

            hence (seq1 . k) = 0 by A1

            .= (seq2 . k) by A2, A4;

          end;

        end;

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let X be non empty ZeroStr, seq be sequence of X;

      :: LOPBAN_4:def5

      func Shift seq -> sequence of X means

      : Def5: (it . 0 ) = ( 0. X) & for k be Nat holds (it . (k + 1)) = (seq . k);

      existence

      proof

        deffunc U( Nat, set) = (seq . $1);

        consider f be sequence of the carrier of X such that

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

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let seq1,seq2 be sequence of X;

        assume that

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

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

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

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

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

        

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

        proof

          let k be Nat;

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

          

          thus (seq1 . (k + 1)) = (seq . k) by A3

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

        end;

        

         A7: X[ 0 ] by A2, A4;

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

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

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let n;

      let X;

      let z,w be Element of X;

      :: LOPBAN_4:def6

      func Expan (n,z,w) -> sequence of X means

      : Def6: for k be Nat holds (k <= n implies (it . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) & (n < k implies (it . k) = ( 0. X));

      existence

      proof

        deffunc U( Nat, Nat) = (((( Coef $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)));

        for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1, seq2;

        assume that

         A1: for k holds (k <= n implies (seq1 . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq1 . k) = ( 0. X)) and

         A2: for k holds (k <= n implies (seq2 . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq2 . k) = ( 0. X));

        now

          let k be Element of NAT ;

          per cases ;

            suppose

             A3: k <= n;

            

            hence (seq1 . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k))) by A1

            .= (seq2 . k) by A2, A3;

          end;

            suppose

             A4: k > n;

            

            hence (seq1 . k) = ( 0. X) by A1

            .= (seq2 . k) by A2, A4;

          end;

        end;

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let n;

      let X;

      let z,w be Element of X;

      :: LOPBAN_4:def7

      func Expan_e (n,z,w) -> sequence of X means

      : Def7: for k be Nat holds (k <= n implies (it . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k)))) & (n < k implies (it . k) = ( 0. X));

      existence

      proof

        deffunc U( Nat, Nat) = (((( Coef_e $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)));

        for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1, seq2;

        assume that

         A1: for k holds (k <= n implies (seq1 . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq1 . k) = ( 0. X)) and

         A2: for k holds (k <= n implies (seq2 . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq2 . k) = ( 0. X));

        now

          let k be Element of NAT ;

          per cases ;

            suppose

             A3: k <= n;

            

            hence (seq1 . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k))) by A1

            .= (seq2 . k) by A2, A3;

          end;

            suppose

             A4: k > n;

            

            hence (seq1 . k) = ( 0. X) by A1

            .= (seq2 . k) by A2, A4;

          end;

        end;

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let n;

      let X;

      let z,w be Element of X;

      :: LOPBAN_4:def8

      func Alfa (n,z,w) -> sequence of X means

      : Def8: for k be Nat holds (k <= n implies (it . k) = (((z rExpSeq ) . k) * (( Partial_Sums (w rExpSeq )) . (n -' k)))) & (n < k implies (it . k) = ( 0. X));

      existence

      proof

        deffunc U( Nat, Nat) = (((z rExpSeq ) . $2) * (( Partial_Sums (w rExpSeq )) . ($1 -' $2)));

        for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1, seq2;

        assume that

         A1: for k holds (k <= n implies (seq1 . k) = (((z rExpSeq ) . k) * (( Partial_Sums (w rExpSeq )) . (n -' k)))) & (k > n implies (seq1 . k) = ( 0. X)) and

         A2: for k holds (k <= n implies (seq2 . k) = (((z rExpSeq ) . k) * (( Partial_Sums (w rExpSeq )) . (n -' k)))) & (k > n implies (seq2 . k) = ( 0. X));

        now

          let k be Element of NAT ;

          per cases ;

            suppose

             A3: k <= n;

            

            hence (seq1 . k) = (((z rExpSeq ) . k) * (( Partial_Sums (w rExpSeq )) . (n -' k))) by A1

            .= (seq2 . k) by A2, A3;

          end;

            suppose

             A4: k > n;

            

            hence (seq1 . k) = ( 0. X) by A1

            .= (seq2 . k) by A2, A4;

          end;

        end;

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let X;

      let z,w be Element of X;

      let n be Nat;

      :: LOPBAN_4:def9

      func Conj (n,z,w) -> sequence of X means

      : Def9: for k be Nat holds (k <= n implies (it . k) = (((z rExpSeq ) . k) * ((( Partial_Sums (w rExpSeq )) . n) - (( Partial_Sums (w rExpSeq )) . (n -' k))))) & (n < k implies (it . k) = ( 0. X));

      existence

      proof

        deffunc U( Nat, Nat) = (((z rExpSeq ) . $2) * ((( Partial_Sums (w rExpSeq )) . $1) - (( Partial_Sums (w rExpSeq )) . ($1 -' $2))));

        for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1, seq2;

        assume that

         A1: for k holds (k <= n implies (seq1 . k) = (((z rExpSeq ) . k) * ((( Partial_Sums (w rExpSeq )) . n) - (( Partial_Sums (w rExpSeq )) . (n -' k))))) & (k > n implies (seq1 . k) = ( 0. X)) and

         A2: for k holds (k <= n implies (seq2 . k) = (((z rExpSeq ) . k) * ((( Partial_Sums (w rExpSeq )) . n) - (( Partial_Sums (w rExpSeq )) . (n -' k))))) & (k > n implies (seq2 . k) = ( 0. X));

        now

          let k be Element of NAT ;

          per cases ;

            suppose

             A3: k <= n;

            

            hence (seq1 . k) = (((z rExpSeq ) . k) * ((( Partial_Sums (w rExpSeq )) . n) - (( Partial_Sums (w rExpSeq )) . (n -' k)))) by A1

            .= (seq2 . k) by A2, A3;

          end;

            suppose

             A4: k > n;

            

            hence (seq1 . k) = ( 0. X) by A1

            .= (seq2 . k) by A2, A4;

          end;

        end;

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    theorem :: LOPBAN_4:14

    

     Th14: ((z rExpSeq ) . (n + 1)) = (((1 / (n + 1)) * z) * ((z rExpSeq ) . n)) & ((z rExpSeq ) . 0 ) = ( 1. X) & ||.((z rExpSeq ) . n).|| <= (( ||.z.|| rExpSeq ) . n)

    proof

      defpred X[ Nat] means ||.((z rExpSeq ) . $1).|| <= (( ||.z.|| rExpSeq ) . $1);

      

       A1: ((z rExpSeq ) . 0 ) = ((1 / ( 0 ! )) * (z #N 0 )) by Def2

      .= ((1 / 1) * ( 1. X)) by LOPBAN_3:def 9, NEWTON: 12

      .= ( 1. X) by RLVECT_1:def 8;

       A2:

      now

        let n be Nat;

        

        thus ((z rExpSeq ) . (n + 1)) = ((1 / ((n + 1) ! )) * (z #N (n + 1))) by Def2

        .= ((1 / ((n + 1) ! )) * (((z GeoSeq ) . n) * z)) by LOPBAN_3:def 9

        .= ((1 / ((n ! ) * (n + 1))) * ((z #N n) * z)) by NEWTON: 15

        .= (((1 * 1) / ((n ! ) * (n + 1))) * (z * (z #N n))) by Lm1

        .= (((1 / (n ! )) * (1 / (n + 1))) * (z * (z #N n))) by XCMPLX_1: 76

        .= (((1 / (n + 1)) * z) * ((1 / (n ! )) * (z #N n))) by LOPBAN_3: 38

        .= (((1 / (n + 1)) * z) * ((z rExpSeq ) . n)) by Def2;

      end;

      

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

      proof

        let n such that

         A4: X[n];

         0 <= ||.((1 / (n + 1)) * z).|| by NORMSP_1: 4;

        then

         A5: ( ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq ) . n).||) <= ( ||.((1 / (n + 1)) * z).|| * (( ||.z.|| rExpSeq ) . n)) by A4, XREAL_1: 64;

        

         A6: ||.(((1 / (n + 1)) * z) * ((z rExpSeq ) . n)).|| <= ( ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq ) . n).||) by LOPBAN_3: 38;

        

         A7: (((1 / (n + 1)) * ||.z.||) * (( ||.z.|| rExpSeq ) . n)) = ((1 / (n + 1)) * ((( ||.z.|| rExpSeq ) . n) * ||.z.||))

        .= ((1 / (n + 1)) * ((( ||.z.|| |^ n) / (n ! )) * ||.z.||)) by SIN_COS:def 5

        .= ((1 / (n + 1)) * ((( ||.z.|| |^ n) * ||.z.||) / (n ! ))) by XCMPLX_1: 74

        .= ((1 / (n + 1)) * (( ||.z.|| |^ (n + 1)) / (n ! ))) by NEWTON: 6

        .= (( ||.z.|| |^ (n + 1)) / ((n ! ) * (n + 1))) by XCMPLX_1: 103

        .= (( ||.z.|| |^ (n + 1)) / ((n + 1) ! )) by NEWTON: 15

        .= (( ||.z.|| rExpSeq ) . (n + 1)) by SIN_COS:def 5;

        

         A8: ||.((1 / (n + 1)) * z).|| = ( |.(1 / (n + 1)).| * ||.z.||) by NORMSP_1:def 1

        .= ((1 / (n + 1)) * ||.z.||) by ABSVALUE:def 1;

         ||.((z rExpSeq ) . (n + 1)).|| = ||.(((1 / (n + 1)) * z) * ((z rExpSeq ) . n)).|| by A2;

        hence thesis by A6, A8, A5, A7, XXREAL_0: 2;

      end;

      (( ||.z.|| rExpSeq ) . 0 ) = (( ||.z.|| |^ 0 ) / ( 0 ! )) by SIN_COS:def 5

      .= (1 / ( 0 ! )) by NEWTON: 4

      .= (1 / ( Prod_real_n . 0 )) by SIN_COS:def 3

      .= (1 / 1) by SIN_COS:def 2

      .= 1;

      then

       A9: X[ 0 ] by A1, LOPBAN_3: 38;

      for n holds X[n] from NAT_1:sch 2( A9, A3);

      hence thesis by A2, A1;

    end;

    theorem :: LOPBAN_4:15

    

     Th15: for X be non empty ZeroStr, seq be sequence of X holds 0 < k implies (( Shift seq) . k) = (seq . (k -' 1))

    proof

      let X be non empty ZeroStr, seq be sequence of X;

      

       A1: k in NAT by ORDINAL1:def 12;

      assume

       A2: 0 < k;

      then

       A3: ( 0 + 1) <= k by INT_1: 7, A1;

      consider m be Nat such that

       A4: (m + 1) = k by A2, NAT_1: 6;

      

       A5: m = (k - 1) by A4;

      

      thus (( Shift seq) . k) = (seq . m) by A4, Def5

      .= (seq . (k -' 1)) by A3, A5, XREAL_1: 233;

    end;

    theorem :: LOPBAN_4:16

    

     Th16: (( Partial_Sums seq) . k) = ((( Partial_Sums ( Shift seq)) . k) + (seq . k))

    proof

      defpred X[ Nat] means (( Partial_Sums seq) . $1) = ((( Partial_Sums ( Shift seq)) . $1) + (seq . $1));

      

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

      proof

        let k;

        assume (( Partial_Sums seq) . k) = ((( Partial_Sums ( Shift seq)) . k) + (seq . k));

        

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

        .= (((( Partial_Sums ( Shift seq)) . k) + (( Shift seq) . (k + 1))) + (seq . (k + 1))) by Def5

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

      end;

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

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

      .= ((( Shift seq) . 0 ) + (seq . 0 )) by Def5

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

      then

       A2: X[ 0 ];

      for k holds X[k] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: LOPBAN_4:17

    

     Th17: for z, w st (z,w) are_commutative holds ((z + w) #N n) = (( Partial_Sums ( Expan (n,z,w))) . n)

    proof

      let z, w such that

       A1: (z,w) are_commutative ;

      defpred X[ Nat] means ((z + w) #N $1) = (( Partial_Sums ( Expan ($1,z,w))) . $1);

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n such that

         A3: ((z + w) #N n) = (( Partial_Sums ( Expan (n,z,w))) . n);

        

         A4: n < (n + 1) by XREAL_1: 29;

        

         A5: n in NAT by ORDINAL1:def 12;

        now

          let k be Element of NAT ;

           A6:

          now

             A7:

            now

              assume

               A8: k < (n + 1);

               A9:

              now

                

                 A10: (((k ! ) * ((n -' k) ! )) * ((n + 1) - k)) = ((k ! ) * (((n -' k) ! ) * ((n + 1) - k)));

                

                 A11: ((k + 1) - 1) <= ((n + 1) - 1) by A8, INT_1: 7, A5;

                

                then

                 A12: ((n -' k) + 1) = ((n - k) + 1) by XREAL_1: 233

                .= ((n + 1) - k)

                .= ((n + 1) -' k) by A8, XREAL_1: 233;

                ((n + 1) - k) <> 0 by A8;

                

                then

                 A13: ((n ! ) / ((k ! ) * ((n -' k) ! ))) = (((n ! ) * ((n + 1) - k)) / (((k ! ) * ((n -' k) ! )) * ((n + 1) - k))) by XCMPLX_1: 91

                .= (((n ! ) * ((n + 1) - k)) / ((k ! ) * (((n + 1) -' k) ! ))) by A11, A10, Th13;

                assume

                 A14: k <> 0 ;

                then

                 A15: ( 0 + 1) <= k by INT_1: 7;

                

                then

                 A16: ((k -' 1) + 1) = ((k - 1) + 1) by XREAL_1: 233

                .= k;

                k < (k + 1) by XREAL_1: 29;

                then (k - 1) <= ((k + 1) - 1) by XREAL_1: 9;

                then (k - 1) <= n by A11, XXREAL_0: 2;

                then

                 A17: (k -' 1) <= n by A15, XREAL_1: 233;

                

                then

                 A18: (n -' (k -' 1)) = (n - (k -' 1)) by XREAL_1: 233

                .= (n - (k - 1)) by A15, XREAL_1: 233

                .= ((n + 1) - k)

                .= ((n + 1) -' k) by A8, XREAL_1: 233;

                

                 A19: (n -' (k -' 1)) = (n - (k -' 1)) by A17, XREAL_1: 233

                .= (n - (k - 1)) by A15, XREAL_1: 233

                .= ((n + 1) - k)

                .= ((n + 1) -' k) by A8, XREAL_1: 233;

                ((((k -' 1) ! ) * ((n -' (k -' 1)) ! )) * k) = ((k * ((k -' 1) ! )) * ((n -' (k -' 1)) ! ))

                .= ((k ! ) * (((n + 1) -' k) ! )) by A14, A19, Th13;

                then

                 A20: ((n ! ) / (((k -' 1) ! ) * ((n -' (k -' 1)) ! ))) = (((n ! ) * k) / ((k ! ) * (((n + 1) -' k) ! ))) by A14, XCMPLX_1: 91;

                (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (((( Expan (n,z,w)) * w) . k) + (( Shift (( Expan (n,z,w)) * z)) . k)) by NORMSP_1:def 2

                .= (((( Expan (n,z,w)) . k) * w) + (( Shift (( Expan (n,z,w)) * z)) . k)) by LOPBAN_3:def 6

                .= (((( Expan (n,z,w)) . k) * w) + ((( Expan (n,z,w)) * z) . (k -' 1))) by A14, Th15

                .= (((( Expan (n,z,w)) . k) * w) + ((( Expan (n,z,w)) . (k -' 1)) * z)) by LOPBAN_3:def 6

                .= (((((( Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + ((( Expan (n,z,w)) . (k -' 1)) * z)) by A11, Def6

                .= (((((( Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + ((((( Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z)) by A17, Def6

                .= ((((( Coef n) . k) * (z #N k)) * ((w #N (n -' k)) * w)) + ((((( Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z)) by LOPBAN_3: 38

                .= ((((( Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((( Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z)) by Lm1

                .= ((((( Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((( Coef n) . (k -' 1)) * (z #N (k -' 1))) * ((w #N (n -' (k -' 1))) * z))) by LOPBAN_3: 38

                .= ((((( Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((( Coef n) . (k -' 1)) * (z #N (k -' 1))) * (z * (w #N (n -' (k -' 1)))))) by A1, Lm2

                .= ((((( Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((( Coef n) . (k -' 1)) * (z #N (k -' 1))) * z) * (w #N (n -' (k -' 1))))) by LOPBAN_3: 38

                .= ((((( Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((( Coef n) . (k -' 1)) * ((z #N (k -' 1)) * z)) * (w #N (n -' (k -' 1))))) by LOPBAN_3: 38

                .= ((((( Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((( Coef n) . (k -' 1)) * (z #N ((k -' 1) + 1))) * (w #N (n -' (k -' 1))))) by Lm1;

                

                then

                 A21: (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (((( Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + (((( Coef n) . (k -' 1)) * (z #N k)) * (w #N ((n + 1) -' k)))) by A12, A18, A16, LOPBAN_3: 38

                .= (((( Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + ((( Coef n) . (k -' 1)) * ((z #N k) * (w #N ((n + 1) -' k))))) by LOPBAN_3: 38

                .= (((( Coef n) . k) + (( Coef n) . (k -' 1))) * ((z #N k) * (w #N ((n + 1) -' k)))) by LOPBAN_3: 38;

                ((( Coef n) . k) + (( Coef n) . (k -' 1))) = (((n ! ) / ((k ! ) * ((n -' k) ! ))) + (( Coef n) . (k -' 1))) by A11, Def3

                .= (((n ! ) / ((k ! ) * ((n -' k) ! ))) + ((n ! ) / (((k -' 1) ! ) * ((n -' (k -' 1)) ! )))) by A17, Def3;

                

                then ((( Coef n) . k) + (( Coef n) . (k -' 1))) = ((((n ! ) * ((n + 1) - k)) + ((n ! ) * k)) / ((k ! ) * (((n + 1) -' k) ! ))) by A13, A20, XCMPLX_1: 62

                .= (((n ! ) * (((n + 1) - k) + k)) / ((k ! ) * (((n + 1) -' k) ! )))

                .= (((n + 1) ! ) / ((k ! ) * (((n + 1) -' k) ! ))) by NEWTON: 15

                .= (( Coef (n + 1)) . k) by A8, Def3;

                

                then (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (((( Coef (n + 1)) . k) * (z #N k)) * (w #N ((n + 1) -' k))) by A21, LOPBAN_3: 38

                .= (( Expan ((n + 1),z,w)) . k) by A8, Def6;

                hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k);

              end;

              now

                

                 A22: ((n + 1) -' 0 ) = ((n + 1) - 0 ) by XREAL_1: 233;

                

                then

                 A23: (( Coef (n + 1)) . 0 ) = (((n + 1) ! ) / (( 0 ! ) * ((n + 1) ! ))) by Def3

                .= 1 by NEWTON: 12, XCMPLX_1: 60;

                

                 A24: (n -' 0 ) = (n - 0 ) by XREAL_1: 233;

                

                then

                 A25: (( Coef n) . 0 ) = ((n ! ) / (( 0 ! ) * (n ! ))) by Def3

                .= 1 by NEWTON: 12, XCMPLX_1: 60;

                assume

                 A26: k = 0 ;

                

                then (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (((( Expan (n,z,w)) * w) . 0 ) + (( Shift (( Expan (n,z,w)) * z)) . 0 )) by NORMSP_1:def 2

                .= (((( Expan (n,z,w)) . 0 ) * w) + (( Shift (( Expan (n,z,w)) * z)) . 0 )) by LOPBAN_3:def 6

                .= (((( Expan (n,z,w)) . 0 ) * w) + ( 0. X)) by Def5

                .= ((( Expan (n,z,w)) . 0 ) * w) by LOPBAN_3: 38

                .= ((((( Coef n) . 0 ) * (z #N 0 )) * (w #N (n -' 0 ))) * w) by Def6

                .= (((( Coef n) . 0 ) * (z #N 0 )) * ((w #N (n -' 0 )) * w)) by LOPBAN_3: 38

                .= (((( Coef (n + 1)) . 0 ) * (z #N 0 )) * (w #N ((n + 1) -' 0 ))) by A24, A22, A25, A23, Lm1

                .= (( Expan ((n + 1),z,w)) . k) by A26, Def6;

                hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k);

              end;

              hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k) by A9;

            end;

             A27:

            now

              

               A28: ((n + 1) -' (n + 1)) = ((n + 1) - (n + 1)) by XREAL_1: 233

              .= 0 ;

              

              then

               A29: (( Coef (n + 1)) . (n + 1)) = (((n + 1) ! ) / (((n + 1) ! ) * ( 0 ! ))) by Def3

              .= 1 by NEWTON: 12, XCMPLX_1: 60;

              

               A30: (n -' n) = (n - n) by XREAL_1: 233

              .= 0 ;

              

              then

               A31: (( Coef n) . n) = ((n ! ) / ((n ! ) * ( 0 ! ))) by Def3

              .= 1 by NEWTON: 12, XCMPLX_1: 60;

              

               A32: n < (n + 1) by XREAL_1: 29;

              assume

               A33: k = (n + 1);

              

              then (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (((( Expan (n,z,w)) * w) . (n + 1)) + (( Shift (( Expan (n,z,w)) * z)) . (n + 1))) by NORMSP_1:def 2

              .= (((( Expan (n,z,w)) . (n + 1)) * w) + (( Shift (( Expan (n,z,w)) * z)) . (n + 1))) by LOPBAN_3:def 6

              .= ((( 0. X) * w) + (( Shift (( Expan (n,z,w)) * z)) . (n + 1))) by A32, Def6

              .= (( 0. X) + (( Shift (( Expan (n,z,w)) * z)) . (n + 1))) by LOPBAN_3: 38

              .= (( Shift (( Expan (n,z,w)) * z)) . (n + 1)) by LOPBAN_3: 38

              .= ((( Expan (n,z,w)) * z) . n) by Def5

              .= ((( Expan (n,z,w)) . n) * z) by LOPBAN_3:def 6

              .= ((((( Coef n) . n) * (z #N n)) * (w #N (n -' n))) * z) by Def6

              .= (((( Coef n) . n) * (z #N n)) * ((w #N (n -' n)) * z)) by LOPBAN_3: 38

              .= (((( Coef n) . n) * (z #N n)) * (z * (w #N (n -' n)))) by A1, Lm2

              .= ((((( Coef n) . n) * (z #N n)) * z) * (w #N (n -' n))) by LOPBAN_3: 38

              .= (((( Coef n) . n) * ((z #N n) * z)) * (w #N (n -' n))) by LOPBAN_3: 38

              .= (((( Coef (n + 1)) . (n + 1)) * (z #N (n + 1))) * (w #N (n -' n))) by A31, A29, Lm1

              .= (( Expan ((n + 1),z,w)) . k) by A33, A30, A28, Def6;

              hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k);

            end;

            assume k <= (n + 1);

            hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k) by A27, A7, XXREAL_0: 1;

          end;

          now

            assume

             A34: (n + 1) < k;

            then

             A35: ((n + 1) - 1) < (k - 1) by XREAL_1: 9;

            then

             A36: (n + 0 ) < ((k - 1) + 1) by XREAL_1: 8;

            ( 0 + 1) <= (n + 1) by XREAL_1: 6;

            then

             A37: (k - 1) = (k -' 1) by A34, XREAL_1: 233, XXREAL_0: 2;

            (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (((( Expan (n,z,w)) * w) . k) + (( Shift (( Expan (n,z,w)) * z)) . k)) by NORMSP_1:def 2

            .= (((( Expan (n,z,w)) . k) * w) + (( Shift (( Expan (n,z,w)) * z)) . k)) by LOPBAN_3:def 6

            .= (((( Expan (n,z,w)) . k) * w) + ((( Expan (n,z,w)) * z) . (k -' 1))) by A36, Th15

            .= (((( Expan (n,z,w)) . k) * w) + ((( Expan (n,z,w)) . (k -' 1)) * z)) by LOPBAN_3:def 6

            .= ((( 0. X) * w) + ((( Expan (n,z,w)) . (k -' 1)) * z)) by A36, Def6

            .= (( 0. X) + ((( Expan (n,z,w)) . (k -' 1)) * z)) by LOPBAN_3: 38

            .= (( 0. X) + (( 0. X) * z)) by A35, A37, Def6

            .= (( 0. X) + ( 0. X)) by LOPBAN_3: 38

            .= ( 0. X) by LOPBAN_3: 38;

            hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k) by A34, Def6;

          end;

          hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k) by A6;

        end;

        then

         A38: ((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) = ( Expan ((n + 1),z,w)) by FUNCT_2: 63;

        

         A39: n < (n + 1) by XREAL_1: 29;

        (( Partial_Sums (( Expan (n,z,w)) * w)) . (n + 1)) = ((( Partial_Sums (( Expan (n,z,w)) * w)) . n) + ((( Expan (n,z,w)) * w) . (n + 1))) by BHSP_4:def 1

        .= ((( Partial_Sums (( Expan (n,z,w)) * w)) . n) + ((( Expan (n,z,w)) . (n + 1)) * w)) by LOPBAN_3:def 6;

        

        then

         A40: (( Partial_Sums (( Expan (n,z,w)) * w)) . (n + 1)) = ((( Partial_Sums (( Expan (n,z,w)) * w)) . n) + (( 0. X) * w)) by A39, Def6

        .= ((( Partial_Sums (( Expan (n,z,w)) * w)) . n) + ( 0. X)) by LOPBAN_3: 38

        .= (( Partial_Sums (( Expan (n,z,w)) * w)) . n) by LOPBAN_3: 38;

        (( Partial_Sums (( Expan (n,z,w)) * z)) . (n + 1)) = ((( Partial_Sums (( Expan (n,z,w)) * z)) . n) + ((( Expan (n,z,w)) * z) . (n + 1))) by BHSP_4:def 1

        .= ((( Partial_Sums (( Expan (n,z,w)) * z)) . n) + ((( Expan (n,z,w)) . (n + 1)) * z)) by LOPBAN_3:def 6;

        

        then

         A41: (( Partial_Sums (( Expan (n,z,w)) * z)) . (n + 1)) = ((( Partial_Sums (( Expan (n,z,w)) * z)) . n) + (( 0. X) * z)) by A4, Def6

        .= ((( Partial_Sums (( Expan (n,z,w)) * z)) . n) + ( 0. X)) by LOPBAN_3: 38

        .= (( Partial_Sums (( Expan (n,z,w)) * z)) . n) by LOPBAN_3: 38;

        ( 0 + n) < (n + 1) by XREAL_1: 29;

        then

         A42: (( Expan (n,z,w)) . (n + 1)) = ( 0. X) by Def6;

        (( Partial_Sums (( Expan (n,z,w)) * z)) . (n + 1)) = ((( Partial_Sums ( Shift (( Expan (n,z,w)) * z))) . (n + 1)) + ((( Expan (n,z,w)) * z) . (n + 1))) by Th16;

        

        then

         A43: (( Partial_Sums (( Expan (n,z,w)) * z)) . (n + 1)) = ((( Partial_Sums ( Shift (( Expan (n,z,w)) * z))) . (n + 1)) + ((( Expan (n,z,w)) . (n + 1)) * z)) by LOPBAN_3:def 6

        .= ((( Partial_Sums ( Shift (( Expan (n,z,w)) * z))) . (n + 1)) + ( 0. X)) by A42, LOPBAN_3: 38

        .= (( Partial_Sums ( Shift (( Expan (n,z,w)) * z))) . (n + 1)) by LOPBAN_3: 38;

        now

          let k be Element of NAT ;

          

          thus ((( Expan (n,z,w)) * (z + w)) . k) = ((( Expan (n,z,w)) . k) * (z + w)) by LOPBAN_3:def 6

          .= (((( Expan (n,z,w)) . k) * z) + ((( Expan (n,z,w)) . k) * w)) by LOPBAN_3: 38

          .= (((( Expan (n,z,w)) * z) . k) + ((( Expan (n,z,w)) . k) * w)) by LOPBAN_3:def 6

          .= (((( Expan (n,z,w)) * z) . k) + ((( Expan (n,z,w)) * w) . k)) by LOPBAN_3:def 6

          .= (((( Expan (n,z,w)) * z) + (( Expan (n,z,w)) * w)) . k) by NORMSP_1:def 2;

        end;

        then

         A44: (( Expan (n,z,w)) * (z + w)) = ((( Expan (n,z,w)) * z) + (( Expan (n,z,w)) * w)) by FUNCT_2: 63;

        ((z + w) #N (n + 1)) = ((((z + w) GeoSeq ) . n) * (z + w)) by LOPBAN_3:def 9

        .= ((( Partial_Sums ( Expan (n,z,w))) * (z + w)) . n) by A3, LOPBAN_3:def 6

        .= (( Partial_Sums (( Expan (n,z,w)) * (z + w))) . n) by Th9;

        

        then ((z + w) #N (n + 1)) = ((( Partial_Sums (( Expan (n,z,w)) * z)) + ( Partial_Sums (( Expan (n,z,w)) * w))) . n) by A44, LOPBAN_3: 15

        .= ((( Partial_Sums (( Expan (n,z,w)) * z)) . n) + (( Partial_Sums (( Expan (n,z,w)) * w)) . n)) by NORMSP_1:def 2;

        

        hence ((z + w) #N (n + 1)) = ((( Partial_Sums (( Expan (n,z,w)) * w)) + ( Partial_Sums ( Shift (( Expan (n,z,w)) * z)))) . (n + 1)) by A41, A40, A43, NORMSP_1:def 2

        .= (( Partial_Sums ( Expan ((n + 1),z,w))) . (n + 1)) by A38, LOPBAN_3: 15;

      end;

      

       A45: ( 0 -' 0 ) = ( 0 - 0 ) by XREAL_0:def 2

      .= 0 ;

      (( Partial_Sums ( Expan ( 0 ,z,w))) . 0 ) = (( Expan ( 0 ,z,w)) . 0 ) by BHSP_4:def 1

      .= (((( Coef 0 ) . 0 ) * (z #N 0 )) * (w #N 0 )) by A45, Def6

      .= (((1 / (1 * 1)) * (z #N 0 )) * (w #N 0 )) by A45, Def3, NEWTON: 12

      .= (((z GeoSeq ) . 0 ) * (w #N 0 )) by RLVECT_1:def 8

      .= (( 1. X) * ((w GeoSeq ) . 0 )) by LOPBAN_3:def 9

      .= (( 1. X) * ( 1. X)) by LOPBAN_3:def 9

      .= ( 1. X) by LOPBAN_3: 38;

      then

       A46: X[ 0 ] by LOPBAN_3:def 9;

      for n holds X[n] from NAT_1:sch 2( A46, A2);

      hence thesis;

    end;

    theorem :: LOPBAN_4:18

    

     Th18: ( Expan_e (n,z,w)) = ((1 / (n ! )) * ( Expan (n,z,w)))

    proof

      now

        let k be Element of NAT ;

         A1:

        now

          

           A2: (1 / ((k ! ) * ((n -' k) ! ))) = ((((n ! ) * 1) / (n ! )) / ((k ! ) * ((n -' k) ! ))) by XCMPLX_1: 60

          .= (((1 / (n ! )) * (n ! )) / ((k ! ) * ((n -' k) ! ))) by XCMPLX_1: 74;

          assume

           A3: k <= n;

          

          hence (( Expan_e (n,z,w)) . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k))) by Def7

          .= (((1 / ((k ! ) * ((n -' k) ! ))) * (z #N k)) * (w #N (n -' k))) by A3, Def4;

          

          hence (( Expan_e (n,z,w)) . k) = ((((1 / (n ! )) * (n ! )) / ((k ! ) * ((n -' k) ! ))) * ((z #N k) * (w #N (n -' k)))) by A2, LOPBAN_3: 38

          .= (((1 / (n ! )) * ((n ! ) / ((k ! ) * ((n -' k) ! )))) * ((z #N k) * (w #N (n -' k)))) by XCMPLX_1: 74

          .= ((1 / (n ! )) * (((n ! ) / ((k ! ) * ((n -' k) ! ))) * ((z #N k) * (w #N (n -' k))))) by LOPBAN_3: 38

          .= ((1 / (n ! )) * ((((n ! ) / ((k ! ) * ((n -' k) ! ))) * (z #N k)) * (w #N (n -' k)))) by LOPBAN_3: 38

          .= ((1 / (n ! )) * (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) by A3, Def3

          .= ((1 / (n ! )) * (( Expan (n,z,w)) . k)) by A3, Def6

          .= (((1 / (n ! )) * ( Expan (n,z,w))) . k) by NORMSP_1:def 5;

        end;

        now

          assume

           A4: n < k;

          

          hence (( Expan_e (n,z,w)) . k) = ( 0. X) by Def7

          .= ((1 / (n ! )) * ( 0. X)) by LOPBAN_3: 38

          .= ((1 / (n ! )) * (( Expan (n,z,w)) . k)) by A4, Def6

          .= (((1 / (n ! )) * ( Expan (n,z,w))) . k) by NORMSP_1:def 5;

        end;

        hence (( Expan_e (n,z,w)) . k) = (((1 / (n ! )) * ( Expan (n,z,w))) . k) by A1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_4:19

    

     Th19: for z, w st (z,w) are_commutative holds ((1 / (n ! )) * ((z + w) #N n)) = (( Partial_Sums ( Expan_e (n,z,w))) . n)

    proof

      let z, w;

      assume (z,w) are_commutative ;

      

      hence ((1 / (n ! )) * ((z + w) #N n)) = ((1 / (n ! )) * (( Partial_Sums ( Expan (n,z,w))) . n)) by Th17

      .= (((1 / (n ! )) * ( Partial_Sums ( Expan (n,z,w)))) . n) by NORMSP_1:def 5

      .= (( Partial_Sums ((1 / (n ! )) * ( Expan (n,z,w)))) . n) by LOPBAN_3: 19

      .= (( Partial_Sums ( Expan_e (n,z,w))) . n) by Th18;

    end;

    theorem :: LOPBAN_4:20

    

     Th20: (( 0. X) rExpSeq ) is norm_summable & ( Sum (( 0. X) rExpSeq )) = ( 1. X)

    proof

      defpred X[ set] means (( Partial_Sums ||.(( 0. X) rExpSeq ).||) . $1) = 1;

      

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

      proof

        let n be Nat such that

         A2: (( Partial_Sums ||.(( 0. X) rExpSeq ).||) . n) = 1;

        

        thus (( Partial_Sums ||.(( 0. X) rExpSeq ).||) . (n + 1)) = (1 + ( ||.(( 0. X) rExpSeq ).|| . (n + 1))) by A2, SERIES_1:def 1

        .= (1 + ||.((( 0. X) rExpSeq ) . (n + 1)).||) by NORMSP_0:def 4

        .= (1 + ||.(((1 / (n + 1)) * ( 0. X)) * ((( 0. X) rExpSeq ) . n)).||) by Th14

        .= (1 + ||.(( 0. X) * ((( 0. X) rExpSeq ) . n)).||) by LOPBAN_3: 38

        .= (1 + ||.( 0. X).||) by LOPBAN_3: 38

        .= (1 + 0 ) by LOPBAN_3: 38

        .= 1;

      end;

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

      .= ||.((( 0. X) rExpSeq ) . 0 ).|| by NORMSP_0:def 4

      .= ||.( 1. X).|| by Th14

      .= 1 by LOPBAN_3: 38;

      then

       A3: X[ 0 ];

      

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

      ( Partial_Sums ||.(( 0. X) rExpSeq ).||) is constant by A4;

      then

       A5: ||.(( 0. X) rExpSeq ).|| is summable by SERIES_1:def 2;

      defpred X[ set] means (( Partial_Sums (( 0. X) rExpSeq )) . $1) = ( 1. X);

      

       A6: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums (( 0. X) rExpSeq )) . n) = ( 1. X);

        

        hence (( Partial_Sums (( 0. X) rExpSeq )) . (n + 1)) = (( 1. X) + ((( 0. X) rExpSeq ) . (n + 1))) by BHSP_4:def 1

        .= (( 1. X) + (((1 / (n + 1)) * ( 0. X)) * ((( 0. X) rExpSeq ) . n))) by Th14

        .= (( 1. X) + (( 0. X) * ((( 0. X) rExpSeq ) . n))) by LOPBAN_3: 38

        .= (( 1. X) + ( 0. X)) by LOPBAN_3: 38

        .= ( 1. X) by LOPBAN_3: 38;

      end;

      (( Partial_Sums (( 0. X) rExpSeq )) . 0 ) = ((( 0. X) rExpSeq ) . 0 ) by BHSP_4:def 1

      .= ( 1. X) by Th14;

      then

       A7: X[ 0 ];

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

      hence thesis by A5, Th2;

    end;

    registration

      let X;

      let z be Element of X;

      cluster (z rExpSeq ) -> norm_summable;

      coherence

      proof

        ex m be Nat st for n be Nat st m <= n holds ||.((z rExpSeq ) . n).|| <= (( ||.z.|| rExpSeq ) . n)

        proof

          take 0 ;

          thus thesis by Th14;

        end;

        hence thesis by LOPBAN_3: 27, SIN_COS: 45;

      end;

    end

    theorem :: LOPBAN_4:21

    

     Th21: ((z rExpSeq ) . 0 ) = ( 1. X) & (( Expan ( 0 ,z,w)) . 0 ) = ( 1. X)

    proof

      

      thus ((z rExpSeq ) . 0 ) = ((1 / ( 0 ! )) * (z #N 0 )) by Def2

      .= ((1 / 1) * ( 1. X)) by LOPBAN_3:def 9, NEWTON: 12

      .= ( 1. X) by LOPBAN_3: 38;

      

       A1: ( 0 -' 0 ) = 0 by XREAL_1: 232;

      

      hence (( Expan ( 0 ,z,w)) . 0 ) = (((( Coef 0 ) . 0 ) * (z #N 0 )) * (w #N 0 )) by Def6

      .= (((1 / (1 * 1)) * (z #N 0 )) * (w #N 0 )) by A1, Def3, NEWTON: 12

      .= (((z GeoSeq ) . 0 ) * (w #N 0 )) by LOPBAN_3: 38

      .= (( 1. X) * ((w GeoSeq ) . 0 )) by LOPBAN_3:def 9

      .= (( 1. X) * ( 1. X)) by LOPBAN_3:def 9

      .= ( 1. X) by LOPBAN_3: 38;

    end;

    theorem :: LOPBAN_4:22

    

     Th22: l <= k implies (( Alfa ((k + 1),z,w)) . l) = ((( Alfa (k,z,w)) . l) + (( Expan_e ((k + 1),z,w)) . l))

    proof

      assume

       A1: l <= k;

      

       A2: k < (k + 1) by XREAL_1: 29;

      then

       A3: l <= (k + 1) by A1, XXREAL_0: 2;

      

       A4: (((z rExpSeq ) . l) * ((w rExpSeq ) . ((k + 1) -' l))) = (((1 / (l ! )) * (z #N l)) * ((w rExpSeq ) . ((k + 1) -' l))) by Def2

      .= (((1 / (l ! )) * (z #N l)) * ((1 / (((k + 1) -' l) ! )) * (w #N ((k + 1) -' l)))) by Def2

      .= (((1 / (l ! )) * (1 / (((k + 1) -' l) ! ))) * ((z #N l) * (w #N ((k + 1) -' l)))) by LOPBAN_3: 38

      .= ((1 / ((l ! ) * (((k + 1) -' l) ! ))) * ((z #N l) * (w #N ((k + 1) -' l)))) by XCMPLX_1: 102

      .= ((( Coef_e (k + 1)) . l) * ((z #N l) * (w #N ((k + 1) -' l)))) by A3, Def4

      .= (((( Coef_e (k + 1)) . l) * (z #N l)) * (w #N ((k + 1) -' l))) by LOPBAN_3: 38

      .= (( Expan_e ((k + 1),z,w)) . l) by A3, Def7;

      ((k + 1) -' l) = ((k + 1) - l) by A1, A2, XREAL_1: 233, XXREAL_0: 2;

      

      then

       A5: ((k + 1) -' l) = ((k - l) + 1)

      .= ((k -' l) + 1) by A1, XREAL_1: 233;

      

      then (( Alfa ((k + 1),z,w)) . l) = (((z rExpSeq ) . l) * (( Partial_Sums (w rExpSeq )) . ((k -' l) + 1))) by A3, Def8

      .= (((z rExpSeq ) . l) * ((( Partial_Sums (w rExpSeq )) . (k -' l)) + ((w rExpSeq ) . ((k + 1) -' l)))) by A5, BHSP_4:def 1

      .= ((((z rExpSeq ) . l) * (( Partial_Sums (w rExpSeq )) . (k -' l))) + (((z rExpSeq ) . l) * ((w rExpSeq ) . ((k + 1) -' l)))) by LOPBAN_3: 38

      .= ((( Alfa (k,z,w)) . l) + (((z rExpSeq ) . l) * ((w rExpSeq ) . ((k + 1) -' l)))) by A1, Def8;

      hence thesis by A4;

    end;

    theorem :: LOPBAN_4:23

    

     Th23: (( Partial_Sums ( Alfa ((k + 1),z,w))) . k) = ((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k))

    proof

      now

        let l be Nat;

        assume l <= k;

        

        hence (( Alfa ((k + 1),z,w)) . l) = ((( Alfa (k,z,w)) . l) + (( Expan_e ((k + 1),z,w)) . l)) by Th22

        .= ((( Alfa (k,z,w)) + ( Expan_e ((k + 1),z,w))) . l) by NORMSP_1:def 2;

      end;

      

      hence (( Partial_Sums ( Alfa ((k + 1),z,w))) . k) = (( Partial_Sums (( Alfa (k,z,w)) + ( Expan_e ((k + 1),z,w)))) . k) by Th11

      .= ((( Partial_Sums ( Alfa (k,z,w))) + ( Partial_Sums ( Expan_e ((k + 1),z,w)))) . k) by LOPBAN_3: 15

      .= ((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k)) by NORMSP_1:def 2;

    end;

    theorem :: LOPBAN_4:24

    

     Th24: ((z rExpSeq ) . k) = (( Expan_e (k,z,w)) . k)

    proof

      

       A1: 0 = (k - k);

      then

       A2: ((k -' k) ! ) = 1 by NEWTON: 12, XREAL_1: 233;

      (k -' k) = 0 by A1, XREAL_1: 233;

      

      hence (( Expan_e (k,z,w)) . k) = (((( Coef_e k) . k) * (z #N k)) * (w #N 0 )) by Def7

      .= (((( Coef_e k) . k) * (z #N k)) * ( 1. X)) by LOPBAN_3: 39

      .= ((( Coef_e k) . k) * (z #N k)) by LOPBAN_3: 38

      .= ((1 / ((k ! ) * 1)) * (z #N k)) by A2, Def4

      .= ((z rExpSeq ) . k) by Def2;

    end;

    theorem :: LOPBAN_4:25

    

     Th25: for z, w st (z,w) are_commutative holds (( Partial_Sums ((z + w) rExpSeq )) . n) = (( Partial_Sums ( Alfa (n,z,w))) . n)

    proof

      let z, w such that

       A1: (z,w) are_commutative ;

      defpred X[ Nat] means (( Partial_Sums ((z + w) rExpSeq )) . $1) = (( Partial_Sums ( Alfa ($1,z,w))) . $1);

      

       A2: for k st X[k] holds X[(k + 1)]

      proof

        let k such that

         A3: (( Partial_Sums ((z + w) rExpSeq )) . k) = (( Partial_Sums ( Alfa (k,z,w))) . k);

        ((k + 1) -' (k + 1)) = 0 by XREAL_1: 232;

        

        then (( Alfa ((k + 1),z,w)) . (k + 1)) = (((z rExpSeq ) . (k + 1)) * (( Partial_Sums (w rExpSeq )) . 0 )) by Def8

        .= (((z rExpSeq ) . (k + 1)) * ((w rExpSeq ) . 0 )) by BHSP_4:def 1

        .= (((z rExpSeq ) . (k + 1)) * ( 1. X)) by Th21

        .= ((z rExpSeq ) . (k + 1)) by LOPBAN_3: 38

        .= (( Expan_e ((k + 1),z,w)) . (k + 1)) by Th24;

        

        then

         A4: ((( Partial_Sums ( Expan_e ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1))) = (( Partial_Sums ( Expan_e ((k + 1),z,w))) . (k + 1)) by BHSP_4:def 1

        .= ((1 / ((k + 1) ! )) * ((z + w) #N (k + 1))) by A1, Th19;

        (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1)) = ((( Partial_Sums ( Alfa ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1))) by BHSP_4:def 1

        .= (((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k)) + (( Alfa ((k + 1),z,w)) . (k + 1))) by Th23

        .= ((( Partial_Sums ((z + w) rExpSeq )) . k) + ((( Partial_Sums ( Expan_e ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1)))) by A3, LOPBAN_3: 38;

        

        then (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1)) = ((( Partial_Sums ((z + w) rExpSeq )) . k) + (((z + w) rExpSeq ) . (k + 1))) by A4, Def2

        .= (( Partial_Sums ((z + w) rExpSeq )) . (k + 1)) by BHSP_4:def 1;

        hence (( Partial_Sums ((z + w) rExpSeq )) . (k + 1)) = (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1));

      end;

      

       A5: (( Partial_Sums ((z + w) rExpSeq )) . 0 ) = (((z + w) rExpSeq ) . 0 ) by BHSP_4:def 1

      .= ( 1. X) by Th21;

      

       A6: ( 0 -' 0 ) = 0 by XREAL_1: 232;

      (( Partial_Sums ( Alfa ( 0 ,z,w))) . 0 ) = (( Alfa ( 0 ,z,w)) . 0 ) by BHSP_4:def 1

      .= (((z rExpSeq ) . 0 ) * (( Partial_Sums (w rExpSeq )) . 0 )) by A6, Def8

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

      .= (( 1. X) * ((w rExpSeq ) . 0 )) by Th21

      .= (( 1. X) * ( 1. X)) by Th21

      .= ( 1. X) by LOPBAN_3: 38;

      then

       A7: X[ 0 ] by A5;

      for n holds X[n] from NAT_1:sch 2( A7, A2);

      hence thesis;

    end;

    theorem :: LOPBAN_4:26

    

     Th26: for z, w st (z,w) are_commutative holds (((( Partial_Sums (z rExpSeq )) . k) * (( Partial_Sums (w rExpSeq )) . k)) - (( Partial_Sums ((z + w) rExpSeq )) . k)) = (( Partial_Sums ( Conj (k,z,w))) . k)

    proof

      let z, w;

      assume (z,w) are_commutative ;

      

      then

       A1: (((( Partial_Sums (z rExpSeq )) . k) * (( Partial_Sums (w rExpSeq )) . k)) - (( Partial_Sums ((z + w) rExpSeq )) . k)) = (((( Partial_Sums (z rExpSeq )) . k) * (( Partial_Sums (w rExpSeq )) . k)) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by Th25

      .= (((( Partial_Sums (z rExpSeq )) * (( Partial_Sums (w rExpSeq )) . k)) . k) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by LOPBAN_3:def 6

      .= ((( Partial_Sums ((z rExpSeq ) * (( Partial_Sums (w rExpSeq )) . k))) . k) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by Th9

      .= ((( Partial_Sums ((z rExpSeq ) * (( Partial_Sums (w rExpSeq )) . k))) - ( Partial_Sums ( Alfa (k,z,w)))) . k) by NORMSP_1:def 3

      .= (( Partial_Sums (((z rExpSeq ) * (( Partial_Sums (w rExpSeq )) . k)) - ( Alfa (k,z,w)))) . k) by LOPBAN_3: 16;

      for l be Nat st l <= k holds ((((z rExpSeq ) * (( Partial_Sums (w rExpSeq )) . k)) - ( Alfa (k,z,w))) . l) = (( Conj (k,z,w)) . l)

      proof

        let l be Nat such that

         A2: l <= k;

        

        thus ((((z rExpSeq ) * (( Partial_Sums (w rExpSeq )) . k)) - ( Alfa (k,z,w))) . l) = ((((z rExpSeq ) * (( Partial_Sums (w rExpSeq )) . k)) . l) - (( Alfa (k,z,w)) . l)) by NORMSP_1:def 3

        .= ((((z rExpSeq ) . l) * (( Partial_Sums (w rExpSeq )) . k)) - (( Alfa (k,z,w)) . l)) by LOPBAN_3:def 6

        .= ((((z rExpSeq ) . l) * (( Partial_Sums (w rExpSeq )) . k)) - (((z rExpSeq ) . l) * (( Partial_Sums (w rExpSeq )) . (k -' l)))) by A2, Def8

        .= (((z rExpSeq ) . l) * ((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l)))) by LOPBAN_3: 38

        .= (( Conj (k,z,w)) . l) by A2, Def9;

      end;

      hence thesis by A1, Th11;

    end;

    theorem :: LOPBAN_4:27

    

     Th27: for n be Nat holds 0 <= (( ||.z.|| rExpSeq ) . n)

    proof

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

      

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

      proof

        let k be Nat such that

         A2: P[k];

        

         A3: 0 <= ||.z.|| by NORMSP_1: 4;

        ( ||.z.|| |^ (k + 1)) = (( ||.z.|| |^ k) * ||.z.||) by NEWTON: 6;

        hence thesis by A2, A3;

      end;

      

       A4: P[ 0 ] by NEWTON: 4;

      let n be Nat;

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

      then

       A5: 0 <= ( ||.z.|| |^ n);

      

       A6: (( ||.z.|| |^ n) / (n ! )) = (( ||.z.|| |^ n) * ((n ! ) " )) by XCMPLX_0:def 9;

      thus thesis by A5, A6, SIN_COS:def 5;

    end;

    theorem :: LOPBAN_4:28

    

     Th28: for k be Nat holds ||.(( Partial_Sums (z rExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k) & (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq )) & ||.(( Partial_Sums (z rExpSeq )) . k).|| <= ( Sum ( ||.z.|| rExpSeq ))

    proof

      let k be Nat;

      defpred X[ Nat] means ||.(( Partial_Sums (z rExpSeq )) . $1).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . $1);

      

       A1: (( Partial_Sums ( ||.z.|| rExpSeq )) . 0 ) = (( ||.z.|| rExpSeq ) . 0 ) by SERIES_1:def 1

      .= (( ||.z.|| |^ 0 ) / ( 0 ! )) by SIN_COS:def 5

      .= 1 by NEWTON: 4, NEWTON: 12;

      

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

      proof

        let k be Nat;

        assume ||.(( Partial_Sums (z rExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k);

        then

         A3: ( ||.(( Partial_Sums (z rExpSeq )) . k).|| + (( ||.z.|| rExpSeq ) . (k + 1))) <= ((( Partial_Sums ( ||.z.|| rExpSeq )) . k) + (( ||.z.|| rExpSeq ) . (k + 1))) by XREAL_1: 6;

        

         A4: ||.((( Partial_Sums (z rExpSeq )) . k) + ((z rExpSeq ) . (k + 1))).|| <= ( ||.(( Partial_Sums (z rExpSeq )) . k).|| + ||.((z rExpSeq ) . (k + 1)).||) by LOPBAN_3: 38;

         ||.((z rExpSeq ) . (k + 1)).|| <= (( ||.z.|| rExpSeq ) . (k + 1)) by Th14;

        then

         A5: ( ||.(( Partial_Sums (z rExpSeq )) . k).|| + ||.((z rExpSeq ) . (k + 1)).||) <= ( ||.(( Partial_Sums (z rExpSeq )) . k).|| + (( ||.z.|| rExpSeq ) . (k + 1))) by XREAL_1: 7;

        

         A6: ((( Partial_Sums ( ||.z.|| rExpSeq )) . k) + (( ||.z.|| rExpSeq ) . (k + 1))) = (( Partial_Sums ( ||.z.|| rExpSeq )) . (k + 1)) by SERIES_1:def 1;

         ||.(( Partial_Sums (z rExpSeq )) . (k + 1)).|| = ||.((( Partial_Sums (z rExpSeq )) . k) + ((z rExpSeq ) . (k + 1))).|| by BHSP_4:def 1;

        then ||.(( Partial_Sums (z rExpSeq )) . (k + 1)).|| <= ( ||.(( Partial_Sums (z rExpSeq )) . k).|| + (( ||.z.|| rExpSeq ) . (k + 1))) by A4, A5, XXREAL_0: 2;

        hence thesis by A3, A6, XXREAL_0: 2;

      end;

       ||.(( Partial_Sums (z rExpSeq )) . 0 ).|| = ||.((z rExpSeq ) . 0 ).|| by BHSP_4:def 1

      .= ||.((1 / ( 0 ! )) * (z #N 0 )).|| by Def2

      .= ||.((1 / 1) * ( 1. X)).|| by LOPBAN_3:def 9, NEWTON: 12

      .= ||.( 1. X).|| by LOPBAN_3: 38

      .= 1 by LOPBAN_3: 38;

      then

       A7: X[ 0 ] by A1;

      

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

      hence ||.(( Partial_Sums (z rExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k);

      

       A9: for n be Nat holds 0 <= (( ||.z.|| rExpSeq ) . n) by Th27;

      ( ||.z.|| rExpSeq ) is summable by SIN_COS: 45;

      then

       A10: ( Partial_Sums ( ||.z.|| rExpSeq )) is bounded_above by A9, SERIES_1: 17;

      then (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( lim ( Partial_Sums ( ||.z.|| rExpSeq ))) by A9, SEQ_4: 37, SERIES_1: 16;

      hence (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq )) by SERIES_1:def 3;

      now

        let k be Nat;

        ( lim ( Partial_Sums ( ||.z.|| rExpSeq ))) = ( Sum ( ||.z.|| rExpSeq )) by SERIES_1:def 3;

        hence (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq )) by A9, A10, SEQ_4: 37, SERIES_1: 16;

      end;

      then

       A11: (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq ));

       ||.(( Partial_Sums (z rExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k) by A8;

      hence thesis by A11, XXREAL_0: 2;

    end;

    theorem :: LOPBAN_4:29

    

     Th29: 1 <= ( Sum ( ||.z.|| rExpSeq ))

    proof

       ||.(( Partial_Sums (z rExpSeq )) . 0 ).|| = ||.((z rExpSeq ) . 0 ).|| by BHSP_4:def 1

      .= ||.( 1. X).|| by Th14

      .= 1 by LOPBAN_3: 38;

      hence thesis by Th28;

    end;

    theorem :: LOPBAN_4:30

    

     Th30: |.(( Partial_Sums ( ||.z.|| rExpSeq )) . n).| = (( Partial_Sums ( ||.z.|| rExpSeq )) . n) & (n <= m implies |.((( Partial_Sums ( ||.z.|| rExpSeq )) . m) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n)).| = ((( Partial_Sums ( ||.z.|| rExpSeq )) . m) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n)))

    proof

      for n be Nat holds 0 <= (( ||.z.|| rExpSeq ) . n) by Th27;

      hence thesis by COMSEQ_3: 9;

    end;

    theorem :: LOPBAN_4:31

    

     Th31: |.(( Partial_Sums ||.( Conj (k,z,w)).||) . n).| = (( Partial_Sums ||.( Conj (k,z,w)).||) . n)

    proof

      

       A1: (( Partial_Sums ||.( Conj (k,z,w)).||) . 0 ) = ( ||.( Conj (k,z,w)).|| . 0 ) by SERIES_1:def 1;

       A2:

      now

        let n be Nat;

        ( ||.( Conj (k,z,w)).|| . n) = ||.(( Conj (k,z,w)) . n).|| by NORMSP_0:def 4;

        hence 0 <= ( ||.( Conj (k,z,w)).|| . n) by NORMSP_1: 4;

      end;

      then ( Partial_Sums ||.( Conj (k,z,w)).||) is non-decreasing by SERIES_1: 16;

      then

       A3: (( Partial_Sums ||.( Conj (k,z,w)).||) . 0 ) <= (( Partial_Sums ||.( Conj (k,z,w)).||) . n) by SEQM_3: 6;

       0 <= ( ||.( Conj (k,z,w)).|| . 0 ) by A2;

      hence thesis by A3, A1, ABSVALUE:def 1;

    end;

    theorem :: LOPBAN_4:32

    

     Th32: for p be Real st p > 0 holds ex n st for k st n <= k holds |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| < p

    proof

      let p be Real such that

       A1: p > 0 ;

      reconsider pp = p as Real;

      set p1 = ( min ((pp / (4 * ( Sum ( ||.z.|| rExpSeq )))),(pp / (4 * ( Sum ( ||.w.|| rExpSeq ))))));

      

       A2: 1 <= ( Sum ( ||.z.|| rExpSeq )) by Th29;

      then ( 0 * ( Sum ( ||.z.|| rExpSeq ))) < (4 * ( Sum ( ||.z.|| rExpSeq ))) by XREAL_1: 68;

      then

       A3: ( 0 / (4 * ( Sum ( ||.z.|| rExpSeq )))) < (p / (4 * ( Sum ( ||.z.|| rExpSeq )))) by A1, XREAL_1: 74;

      

       A4: 1 <= ( Sum ( ||.w.|| rExpSeq )) by Th29;

      then ( 0 * ( Sum ( ||.w.|| rExpSeq ))) < (4 * ( Sum ( ||.w.|| rExpSeq ))) by XREAL_1: 68;

      then ( 0 / (4 * ( Sum ( ||.w.|| rExpSeq )))) < (p / (4 * ( Sum ( ||.w.|| rExpSeq )))) by A1, XREAL_1: 74;

      then

       A5: p1 > 0 by A3, XXREAL_0: 15;

      ( Partial_Sums (w rExpSeq )) is convergent by LOPBAN_3:def 1;

      then for s be Real st 0 < s holds ex n be Nat st for m be Nat st n <= m holds ||.((( Partial_Sums (w rExpSeq )) . m) - (( Partial_Sums (w rExpSeq )) . n)).|| < s by LOPBAN_3: 4;

      then ( Partial_Sums (w rExpSeq )) is Cauchy_sequence_by_Norm by LOPBAN_3: 5;

      then

      consider n2 such that

       A6: for k,l be Nat st n2 <= k & n2 <= l holds ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . l)).|| < p1 by A5, RSSPACE3: 8;

      ( ||.z.|| rExpSeq ) is summable by SIN_COS: 45;

      then ( Partial_Sums ( ||.z.|| rExpSeq )) is convergent by SERIES_1:def 2;

      then

      consider n1 be Nat such that

       A7: for k,l be Nat st n1 <= k & n1 <= l holds |.((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . l)).| < p1 by A5, COMSEQ_3: 4;

      set n3 = (n1 + n2);

      take n4 = (n3 + n3);

       A8:

      now

        let n;

        let k be Nat;

        let l be Nat such that

         A9: l <= k;

        

         A10: ||.(((z rExpSeq ) . l) * ((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l)))).|| <= ( ||.((z rExpSeq ) . l).|| * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) by LOPBAN_3: 38;

         0 <= ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).|| by NORMSP_1: 4;

        then

         A11: ( ||.((z rExpSeq ) . l).|| * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) by Th14, XREAL_1: 64;

        ( ||.( Conj (k,z,w)).|| . l) = ||.(( Conj (k,z,w)) . l).|| by NORMSP_0:def 4

        .= ||.(((z rExpSeq ) . l) * ((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l)))).|| by A9, Def9;

        hence ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) by A10, A11, XXREAL_0: 2;

      end;

       A12:

      now

        let k be Nat;

        let l be Nat;

        

         A13: ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).|| <= ( ||.(( Partial_Sums (w rExpSeq )) . k).|| + ||.(( Partial_Sums (w rExpSeq )) . (k -' l)).||) by NORMSP_1: 3;

         ||.(( Partial_Sums (w rExpSeq )) . (k -' l)).|| <= ( Sum ( ||.w.|| rExpSeq )) by Th28;

        then

         A14: (( Sum ( ||.w.|| rExpSeq )) + ||.(( Partial_Sums (w rExpSeq )) . (k -' l)).||) <= (( Sum ( ||.w.|| rExpSeq )) + ( Sum ( ||.w.|| rExpSeq ))) by XREAL_1: 6;

         ||.(( Partial_Sums (w rExpSeq )) . k).|| <= ( Sum ( ||.w.|| rExpSeq )) by Th28;

        then ( ||.(( Partial_Sums (w rExpSeq )) . k).|| + ||.(( Partial_Sums (w rExpSeq )) . (k -' l)).||) <= (( Sum ( ||.w.|| rExpSeq )) + ||.(( Partial_Sums (w rExpSeq )) . (k -' l)).||) by XREAL_1: 6;

        then ( ||.(( Partial_Sums (w rExpSeq )) . k).|| + ||.(( Partial_Sums (w rExpSeq )) . (k -' l)).||) <= (2 * ( Sum ( ||.w.|| rExpSeq ))) by A14, XXREAL_0: 2;

        then

         A15: ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).|| <= (2 * ( Sum ( ||.w.|| rExpSeq ))) by A13, XXREAL_0: 2;

        assume l <= k;

        then

         A16: ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) by A8;

         0 <= (( ||.z.|| rExpSeq ) . l) by Th27;

        then ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) <= ((( ||.z.|| rExpSeq ) . l) * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A15, XREAL_1: 64;

        hence ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A16, XXREAL_0: 2;

      end;

      now

         0 < (p / 4) by A1, XREAL_1: 224;

        then

         A17: ( 0 + (p / 4)) < ((p / 4) + (p / 4)) by XREAL_1: 6;

        

         A18: 0 <> ( Sum ( ||.z.|| rExpSeq )) by Th29;

        

         A19: (( Sum ( ||.z.|| rExpSeq )) * (p / (4 * ( Sum ( ||.z.|| rExpSeq ))))) = (( Sum ( ||.z.|| rExpSeq )) * (p * ((4 * ( Sum ( ||.z.|| rExpSeq ))) " ))) by XCMPLX_0:def 9

        .= ((( Sum ( ||.z.|| rExpSeq )) * p) * ((4 * ( Sum ( ||.z.|| rExpSeq ))) " ))

        .= ((( Sum ( ||.z.|| rExpSeq )) * p) / (4 * ( Sum ( ||.z.|| rExpSeq )))) by XCMPLX_0:def 9

        .= (p / 4) by A18, XCMPLX_1: 91;

        let k such that

         A20: n4 <= k;

        

         A21: ( 0 + n3) <= (n3 + n3) by XREAL_1: 6;

        then (k -' n3) = (k - n3) by A20, XREAL_1: 233, XXREAL_0: 2;

        then

         A22: k = ((k -' n3) + n3);

        

         A23: n3 <= k by A20, A21, XXREAL_0: 2;

        now

          let l be Nat;

          

           A24: ( 0 + n2) <= (n1 + n2) by XREAL_1: 6;

          ( 0 + n3) <= (n3 + n3) by XREAL_1: 6;

          then n2 <= n4 by A24, XXREAL_0: 2;

          then

           A25: n2 <= k by A20, XXREAL_0: 2;

          

           A26: 0 <= (( ||.z.|| rExpSeq ) . l) by Th27;

          assume

           A27: l <= n3;

          then

           A28: ((n3 + n3) - n3) <= ((n3 + n3) - l) by XREAL_1: 10;

          l <= k by A23, A27, XXREAL_0: 2;

          then

           A29: ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) by A8;

          (n4 - l) <= (k - l) by A20, XREAL_1: 9;

          then

           A30: n3 <= (k - l) by A28, XXREAL_0: 2;

          (k -' l) = (k - l) by A23, A27, XREAL_1: 233, XXREAL_0: 2;

          then n2 <= (k -' l) by A24, A30, XXREAL_0: 2;

          then ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).|| < p1 by A6, A25;

          then ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w rExpSeq )) . k) - (( Partial_Sums (w rExpSeq )) . (k -' l))).||) <= ((( ||.z.|| rExpSeq ) . l) * p1) by A26, XREAL_1: 64;

          hence ( ||.( Conj (k,z,w)).|| . l) <= (p1 * (( ||.z.|| rExpSeq ) . l)) by A29, XXREAL_0: 2;

        end;

        then

         A31: (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) <= ((( Partial_Sums ( ||.z.|| rExpSeq )) . n3) * p1) by COMSEQ_3: 7;

        

         A32: (n1 + 0 ) <= (n1 + n2) by XREAL_1: 6;

        then n1 <= k by A23, XXREAL_0: 2;

        then |.((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)).| <= p1 by A7, A32;

        then ((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)) <= p1 by A20, A21, Th30, XXREAL_0: 2;

        then

         A33: (((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)) * (2 * ( Sum ( ||.w.|| rExpSeq )))) <= (p1 * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A4, XREAL_1: 64;

        for l be Nat st l <= k holds ( ||.( Conj (k,z,w)).|| . l) <= ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (( ||.z.|| rExpSeq ) . l)) by A12;

        then ((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) <= (((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)) * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A22, COMSEQ_3: 8;

        then

         A34: ((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) <= (p1 * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A33, XXREAL_0: 2;

        

         A35: 0 <> ( Sum ( ||.w.|| rExpSeq )) by Th29;

        ((( Partial_Sums ( ||.z.|| rExpSeq )) . n3) * p1) <= (( Sum ( ||.z.|| rExpSeq )) * p1) by A5, Th28, XREAL_1: 64;

        then

         A36: (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) <= (( Sum ( ||.z.|| rExpSeq )) * p1) by A31, XXREAL_0: 2;

        (( Sum ( ||.z.|| rExpSeq )) * p1) <= (( Sum ( ||.z.|| rExpSeq )) * (p / (4 * ( Sum ( ||.z.|| rExpSeq ))))) by A2, XREAL_1: 64, XXREAL_0: 17;

        then (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) <= (p / 4) by A36, A19, XXREAL_0: 2;

        then

         A37: (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) < (p / 2) by A17, XXREAL_0: 2;

        ( 0 * ( Sum ( ||.w.|| rExpSeq ))) < (2 * ( Sum ( ||.w.|| rExpSeq ))) by A4, XREAL_1: 68;

        then

         A38: ((2 * ( Sum ( ||.w.|| rExpSeq ))) * p1) <= ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (p / (4 * ( Sum ( ||.w.|| rExpSeq ))))) by XREAL_1: 64, XXREAL_0: 17;

        ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (p / (4 * ( Sum ( ||.w.|| rExpSeq ))))) = ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (p * ((4 * ( Sum ( ||.w.|| rExpSeq ))) " ))) by XCMPLX_0:def 9

        .= (((2 * ( Sum ( ||.w.|| rExpSeq ))) * p) * ((4 * ( Sum ( ||.w.|| rExpSeq ))) " ))

        .= (((2 * p) * ( Sum ( ||.w.|| rExpSeq ))) / (4 * ( Sum ( ||.w.|| rExpSeq )))) by XCMPLX_0:def 9

        .= ((2 * p) / 4) by A35, XCMPLX_1: 91

        .= (p / 2);

        then ((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) <= (p / 2) by A34, A38, XXREAL_0: 2;

        then (((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) + (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) < ((p / 2) + (p / 2)) by A37, XREAL_1: 8;

        hence |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| < p by Th31;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_4:33

    

     Th33: for seq st for k holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k) holds seq is convergent & ( lim seq) = ( 0. X)

    proof

      deffunc U( Nat) = (( Partial_Sums ||.( Conj ($1,z,w)).||) . $1);

      ex rseq be Real_Sequence st for k be Nat holds (rseq . k) = U(k) from SEQ_1:sch 1;

      then

      consider rseq be Real_Sequence such that

       A1: for k be Nat holds (rseq . k) = (( Partial_Sums ||.( Conj (k,z,w)).||) . k);

      let seq such that

       A2: for k holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k);

       A3:

      now

        let k;

         ||.(seq . k).|| = ||.(( Partial_Sums ( Conj (k,z,w))) . k).|| by A2;

        hence ||.(seq . k).|| <= (( Partial_Sums ||.( Conj (k,z,w)).||) . k) by Th10;

      end;

       A4:

      now

        let k;

         ||.(seq . k).|| <= (( Partial_Sums ||.( Conj (k,z,w)).||) . k) by A3;

        hence ||.(seq . k).|| <= (rseq . k) by A1;

      end;

       A5:

      now

        let p be Real;

        assume p > 0 ;

        then

        consider n such that

         A6: for k st n <= k holds |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| < p by Th32;

        reconsider n as Nat;

        take n;

        let k be Nat such that

         A7: n <= k;

         |.((rseq . k) - 0 ).| = |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| by A1;

        hence |.((rseq . k) - 0 ).| < p by A6, A7;

      end;

      then

       A8: rseq is convergent by SEQ_2:def 6;

      then ( lim rseq) = 0 by A5, SEQ_2:def 7;

      hence thesis by A4, A8, Th12;

    end;

    

     Lm3: for z, w st (z,w) are_commutative holds (( Sum (z rExpSeq )) * ( Sum (w rExpSeq ))) = ( Sum ((z + w) rExpSeq ))

    proof

      let z, w such that

       A1: (z,w) are_commutative ;

      deffunc U( Nat) = (( Partial_Sums ( Conj ($1,z,w))) . $1);

      ex seq st for k be Element of NAT holds (seq . k) = U(k) from FUNCT_2:sch 4;

      then

      consider seq be sequence of X such that

       A2: for k be Element of NAT holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k);

      

       A3: for k be Nat holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k)

      proof

        let k be Nat;

        k in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      now

        let k be Element of NAT ;

        

        thus (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k) by A2

        .= (((( Partial_Sums (z rExpSeq )) . k) * (( Partial_Sums (w rExpSeq )) . k)) - (( Partial_Sums ((z + w) rExpSeq )) . k)) by A1, Th26

        .= (((( Partial_Sums (z rExpSeq )) * ( Partial_Sums (w rExpSeq ))) . k) - (( Partial_Sums ((z + w) rExpSeq )) . k)) by LOPBAN_3:def 7

        .= (((( Partial_Sums (z rExpSeq )) * ( Partial_Sums (w rExpSeq ))) - ( Partial_Sums ((z + w) rExpSeq ))) . k) by NORMSP_1:def 3;

      end;

      then

       A4: seq = ((( Partial_Sums (z rExpSeq )) * ( Partial_Sums (w rExpSeq ))) - ( Partial_Sums ((z + w) rExpSeq ))) by FUNCT_2: 63;

      

       A5: ( Partial_Sums (w rExpSeq )) is convergent by LOPBAN_3:def 1;

      

       A6: ( lim seq) = ( 0. X) by A3, Th33;

      

       A7: ( Partial_Sums ((z + w) rExpSeq )) is convergent by LOPBAN_3:def 1;

      

       A8: ( Partial_Sums (z rExpSeq )) is convergent by LOPBAN_3:def 1;

      then

       A9: ( lim (( Partial_Sums (z rExpSeq )) * ( Partial_Sums (w rExpSeq )))) = (( lim ( Partial_Sums (z rExpSeq ))) * ( lim ( Partial_Sums (w rExpSeq )))) by A5, Th8;

      (( Partial_Sums (z rExpSeq )) * ( Partial_Sums (w rExpSeq ))) is convergent by A8, A5, Th3;

      hence thesis by A4, A7, A9, A6, Th1;

    end;

    definition

      let X be Banach_Algebra;

      :: LOPBAN_4:def10

      func exp_ X -> Function of the carrier of X, the carrier of X means

      : Def10: for z be Element of X holds (it . z) = ( Sum (z rExpSeq ));

      existence

      proof

        deffunc U( Element of X) = ( Sum ($1 rExpSeq ));

        ex f be Function of the carrier of X, the carrier of X st for z be Element of X holds (f . z) = U(z) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of the carrier of X, the carrier of X;

        assume that

         A1: for z be Element of X holds (f1 . z) = ( Sum (z rExpSeq )) and

         A2: for z be Element of X holds (f2 . z) = ( Sum (z rExpSeq ));

        for z be Element of X holds (f1 . z) = (f2 . z)

        proof

          let z be Element of X;

          

          thus (f1 . z) = ( Sum (z rExpSeq )) by A1

          .= (f2 . z) by A2;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    definition

      let X, z;

      :: LOPBAN_4:def11

      func exp z -> Element of X equals (( exp_ X) . z);

      correctness ;

    end

    theorem :: LOPBAN_4:34

    for z holds ( exp z) = ( Sum (z rExpSeq )) by Def10;

    theorem :: LOPBAN_4:35

    

     Th35: for z1, z2 st (z1,z2) are_commutative holds ( exp (z1 + z2)) = (( exp z1) * ( exp z2)) & ( exp (z2 + z1)) = (( exp z2) * ( exp z1)) & ( exp (z1 + z2)) = ( exp (z2 + z1)) & (( exp z1),( exp z2)) are_commutative

    proof

      let z1, z2 such that

       A1: (z1,z2) are_commutative ;

      

       A2: ( exp (z2 + z1)) = ( Sum ((z2 + z1) rExpSeq )) by Def10

      .= (( Sum (z2 rExpSeq )) * ( Sum (z1 rExpSeq ))) by A1, Lm3

      .= (( exp z2) * ( Sum (z1 rExpSeq ))) by Def10

      .= (( exp z2) * ( exp z1)) by Def10;

      ( exp (z1 + z2)) = ( Sum ((z1 + z2) rExpSeq )) by Def10

      .= (( Sum (z1 rExpSeq )) * ( Sum (z2 rExpSeq ))) by A1, Lm3

      .= (( exp z1) * ( Sum (z2 rExpSeq ))) by Def10

      .= (( exp z1) * ( exp z2)) by Def10;

      hence thesis by A2;

    end;

    theorem :: LOPBAN_4:36

    for z1, z2 st (z1,z2) are_commutative holds (z1 * ( exp z2)) = (( exp z2) * z1)

    proof

      let z1, z2 such that

       A1: (z1,z2) are_commutative ;

      now

        let n be Element of NAT ;

        

        thus ((z1 * (z2 rExpSeq )) . n) = (z1 * ((z2 rExpSeq ) . n)) by LOPBAN_3:def 5

        .= (z1 * ((1 / (n ! )) * (z2 #N n))) by Def2

        .= ((1 / (n ! )) * (z1 * (z2 #N n))) by LOPBAN_3: 38

        .= ((1 / (n ! )) * ((z2 #N n) * z1)) by A1, Lm2

        .= (((1 / (n ! )) * (z2 #N n)) * z1) by LOPBAN_3: 38

        .= (((z2 rExpSeq ) . n) * z1) by Def2

        .= (((z2 rExpSeq ) * z1) . n) by LOPBAN_3:def 6;

      end;

      then

       A2: (z1 * (z2 rExpSeq )) = ((z2 rExpSeq ) * z1) by FUNCT_2: 63;

      

       A3: ( Partial_Sums (z2 rExpSeq )) is convergent by LOPBAN_3:def 1;

      

      thus (z1 * ( exp z2)) = (z1 * ( Sum (z2 rExpSeq ))) by Def10

      .= ( lim (z1 * ( Partial_Sums (z2 rExpSeq )))) by A3, Th6

      .= ( lim ( Partial_Sums (z1 * (z2 rExpSeq )))) by Th9

      .= ( lim (( Partial_Sums (z2 rExpSeq )) * z1)) by A2, Th9

      .= (( Sum (z2 rExpSeq )) * z1) by A3, Th7

      .= (( exp z2) * z1) by Def10;

    end;

    theorem :: LOPBAN_4:37

    

     Th37: ( exp ( 0. X)) = ( 1. X)

    proof

      ( exp ( 0. X)) = ( Sum (( 0. X) rExpSeq )) by Def10

      .= ( 1. X) by Th20;

      hence thesis;

    end;

    theorem :: LOPBAN_4:38

    

     Th38: (( exp z) * ( exp ( - z))) = ( 1. X) & (( exp ( - z)) * ( exp z)) = ( 1. X)

    proof

      reconsider jj = 1 as Real;

      (z * ( - z)) = (z * (( - jj) * z)) by LOPBAN_3: 38

      .= (( - jj) * (z * z)) by LOPBAN_3: 38

      .= ((( - jj) * z) * z) by LOPBAN_3: 38

      .= (( - z) * z) by LOPBAN_3: 38;

      then

       A1: (z,( - z)) are_commutative ;

      

      hence (( exp z) * ( exp ( - z))) = ( exp (z + ( - z))) by Th35

      .= ( exp ( 0. X)) by RLVECT_1: 5

      .= ( 1. X) by Th37;

      

      thus (( exp ( - z)) * ( exp z)) = ( exp (( - z) + z)) by A1, Th35

      .= ( exp ( 0. X)) by RLVECT_1: 5

      .= ( 1. X) by Th37;

    end;

    theorem :: LOPBAN_4:39

    ( exp z) is invertible & (( exp z) " ) = ( exp ( - z)) & ( exp ( - z)) is invertible & (( exp ( - z)) " ) = ( exp z)

    proof

      

       A1: (( exp ( - z)) * ( exp z)) = ( 1. X) by Th38;

      

       A2: (( exp z) * ( exp ( - z))) = ( 1. X) by Th38;

      hence ( exp z) is invertible by A1;

      hence (( exp z) " ) = ( exp ( - z)) by A2, A1, LOPBAN_3:def 8;

      thus ( exp ( - z)) is invertible by A2, A1;

      hence thesis by A2, A1, LOPBAN_3:def 8;

    end;

    theorem :: LOPBAN_4:40

    

     Th40: for z holds for s,t be Real holds ((s * z),(t * z)) are_commutative

    proof

      let z;

      let s,t be Real;

      ((s * z) * (t * z)) = ((s * t) * (z * z)) by LOPBAN_3: 38

      .= ((t * z) * (s * z)) by LOPBAN_3: 38;

      hence thesis;

    end;

    theorem :: LOPBAN_4:41

    for z holds for s,t be Real holds (( exp (s * z)) * ( exp (t * z))) = ( exp ((s + t) * z)) & (( exp (t * z)) * ( exp (s * z))) = ( exp ((t + s) * z)) & ( exp ((s + t) * z)) = ( exp ((t + s) * z)) & (( exp (s * z)),( exp (t * z))) are_commutative

    proof

      let z;

      let s,t be Real;

      

       A1: ((s * z),(t * z)) are_commutative by Th40;

      

      hence

       A2: (( exp (s * z)) * ( exp (t * z))) = ( exp ((s * z) + (t * z))) by Th35

      .= ( exp ((s + t) * z)) by LOPBAN_3: 38;

      

      thus

       A3: (( exp (t * z)) * ( exp (s * z))) = ( exp ((t * z) + (s * z))) by A1, Th35

      .= ( exp ((t + s) * z)) by LOPBAN_3: 38;

      thus ( exp ((s + t) * z)) = ( exp ((t + s) * z));

      thus thesis by A2, A3;

    end;