lp_space.miz

    begin

    definition

      let x be Real_Sequence;

      let p be Real;

      :: LP_SPACE:def1

      func x rto_power p -> Real_Sequence means

      : Def1: for n be Nat holds (it . n) = ( |.(x . n).| to_power p);

      existence

      proof

        deffunc F( set) = ( |.(x . $1).| to_power p);

        ex q1 be Real_Sequence st for n be Nat holds (q1 . n) = F(n) from SEQ_1:sch 1;

        then

        consider q1 be Real_Sequence such that

         A1: for n be Nat holds (q1 . n) = ( |.(x . n).| to_power p);

        take q1;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let a1,a2 be Real_Sequence;

        assume that

         A2: for n be Nat holds (a1 . n) = ( |.(x . n).| to_power p) and

         A3: for n be Nat holds (a2 . n) = ( |.(x . n).| to_power p);

        for s be object st s in NAT holds (a1 . s) = (a2 . s)

        proof

          let s be object such that

           A4: s in NAT ;

          (a1 . s) = ( |.(x . s).| to_power p) by A2, A4

          .= (a2 . s) by A3, A4;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    definition

      let p be Real;

      assume

       A1: p >= 1;

      :: LP_SPACE:def2

      func the_set_of_RealSequences_l^ p -> non empty Subset of Linear_Space_of_RealSequences means

      : Def2: for x be set holds x in it iff x in the_set_of_RealSequences & (( seq_id x) rto_power p) is summable;

      existence

      proof

        defpred P[ object] means (( seq_id $1) rto_power p) is summable;

        consider IT be set such that

         A2: for x be object holds x in IT iff x in the_set_of_RealSequences & P[x] from XBOOLE_0:sch 1;

        for x be object st x in IT holds x in the_set_of_RealSequences by A2;

        then

         A3: IT is Subset of the_set_of_RealSequences by TARSKI:def 3;

        (( seq_id Zeroseq ) rto_power p) is absolutely_summable

        proof

          reconsider rseq = (( seq_id Zeroseq ) rto_power p) as Real_Sequence;

          now

            let n be Nat;



            thus (rseq . n) = ( |.(( seq_id Zeroseq ) . n).| to_power p) by Def1

            .= ( 0 to_power p) by ABSVALUE: 2, RSSPACE: 4

            .= 0 by A1, POWER:def 2;

          end;

          hence thesis by COMSEQ_3: 3;

        end;

        then IT is non empty by A2;

        then

        reconsider IT as non empty Subset of Linear_Space_of_RealSequences by A3;

        take IT;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let X1,X2 be non empty Subset of Linear_Space_of_RealSequences ;

        assume that

         A4: for x be set holds x in X1 iff x in the_set_of_RealSequences & (( seq_id x) rto_power p) is summable and

         A5: for x be set holds x in X2 iff x in the_set_of_RealSequences & (( seq_id x) rto_power p) is summable;



         A6: X2 c= X1

        proof

          let x be object;

          assume

           A7: x in X2;

          then

           A8: (( seq_id x) rto_power p) is summable by A5;

          x in the_set_of_RealSequences by A7;

          hence thesis by A4, A8;

        end;

        X1 c= X2

        proof

          let x be object;

          assume

           A9: x in X1;

          then

           A10: (( seq_id x) rto_power p) is summable by A4;

          x in the_set_of_RealSequences by A9;

          hence thesis by A5, A10;

        end;

        hence thesis by A6, XBOOLE_0:def 10;

      end;

    end

    reserve x1,x2,y1,a,b,c for Real;



     Lm1: x1 >= 0 & y1 > 0 implies (x1 to_power y1) >= 0

    proof

      assume that

       A1: x1 >= 0 and

       A2: y1 > 0 ;

      x1 > 0 or x1 = 0 by A1;

      hence thesis by A2, POWER: 34, POWER:def 2;

    end;



     Lm2: y1 > 0 & x1 >= 0 & x2 >= 0 implies ((x1 * x2) to_power y1) = ((x1 to_power y1) * (x2 to_power y1))

    proof

      assume that

       A1: y1 > 0 and

       A2: x1 >= 0 and

       A3: x2 >= 0 ;

      per cases by A2, A3;

        suppose x1 > 0 & x2 > 0 ;

        hence thesis by POWER: 30;

      end;

        suppose

         A4: x1 > 0 & x2 = 0 ;

        then (x2 to_power y1) = 0 by A1, POWER:def 2;

        hence thesis by A4;

      end;

        suppose

         A5: x1 = 0 & x2 > 0 ;

        then (x1 to_power y1) = 0 by A1, POWER:def 2;

        hence thesis by A5;

      end;

        suppose

         A6: x1 = 0 & x2 = 0 ;

        then (x2 to_power y1) = 0 by A1, POWER:def 2;

        hence thesis by A6;

      end;

    end;

    theorem :: LP_SPACE:1



     Th1: a >= 0 & a < b & c > 0 implies (a to_power c) < (b to_power c)

    proof

      a = 0 & c > 0 implies (a to_power c) = 0 by POWER:def 2;

      hence thesis by POWER: 34, POWER: 37;

    end;



     Lm3: for p be Real st 1 = p holds for a,b be Real_Sequence holds for n be Nat holds ((( Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p)) <= (((( Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + ((( Partial_Sums (b rto_power p)) . n) to_power (1 / p)))

    proof

      let p be Real such that

       A1: p = 1;

      let a,b be Real_Sequence;

      let n be Nat;

       A2:

      now

        let n be Nat;



        thus (((a + b) rto_power p) . n) = ( |.((a + b) . n).| to_power p) by Def1

        .= |.((a + b) . n).| by A1, POWER: 25;



        thus ((a rto_power p) . n) = ( |.(a . n).| to_power p) by Def1

        .= |.(a . n).| by A1, POWER: 25;



        thus ((b rto_power p) . n) = ( |.(b . n).| to_power p) by Def1

        .= |.(b . n).| by A1, POWER: 25;

      end;

      then ((a + b) rto_power p) = |.(a + b).| by SEQ_1: 12;

      then

       A3: ((( Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p)) = (( Partial_Sums ( abs (a + b))) . n) by A1, POWER: 25;

      (a rto_power p) = |.a.| by A2, SEQ_1: 12;

      then

       A4: ((( Partial_Sums (a rto_power p)) . n) to_power (1 / p)) = (( Partial_Sums |.a.|) . n) by A1, POWER: 25;

      deffunc F( Nat) = ( |.(a . $1).| + |.(b . $1).|);

      consider c be Real_Sequence such that

       A5: for n be Nat holds (c . n) = F(n) from SEQ_1:sch 1;



       A6: for n be Nat holds |.((a + b) . n).| <= ( |.(b . n).| + |.(a . n).|)

      proof

        let n be Nat;

         |.((a + b) . n).| = |.((a . n) + (b . n)).| by SEQ_1: 7;

        hence thesis by COMPLEX1: 56;

      end;

      now

        let n be Nat;



         A7: |.((a + b) . n).| = (( abs (a + b)) . n) by SEQ_1: 12;

         |.((a + b) . n).| <= ( |.(b . n).| + |.(a . n).|) by A6;

        hence (( abs (a + b)) . n) <= (c . n) by A5, A7;

      end;

      then

       A8: (( Partial_Sums ( abs (a + b))) . n) <= (( Partial_Sums c) . n) by SERIES_1: 14;

      now

        let n be Nat;



         A9: |.(a . n).| = (( abs a) . n) by SEQ_1: 12;

         |.(b . n).| = (( abs b) . n) by SEQ_1: 12;



        hence (c . n) = ((( abs a) . n) + (( abs b) . n)) by A5, A9

        .= ((( abs a) + ( abs b)) . n) by SEQ_1: 7;

      end;

      then for n be object st n in NAT holds (c . n) = ((( abs a) + ( abs b)) . n);

      then

       A10: c = (( abs a) + ( abs b)) by FUNCT_2: 12;

      (b rto_power p) = |.b.| by A2, SEQ_1: 12;

      then

       A11: ((( Partial_Sums (b rto_power p)) . n) to_power (1 / p)) = (( Partial_Sums |.b.|) . n) by A1, POWER: 25;

      ( Partial_Sums (( abs a) + ( abs b))) = (( Partial_Sums ( abs a)) + ( Partial_Sums |.b.|)) by SERIES_1: 5;

      hence thesis by A3, A4, A11, A10, A8, SEQ_1: 7;

    end;

    theorem :: LP_SPACE:2



     Th2: for p be Real st 1 <= p holds for a,b be Real_Sequence holds for n be Nat holds ((( Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p)) <= (((( Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + ((( Partial_Sums (b rto_power p)) . n) to_power (1 / p)))

    proof

      let p be Real such that

       A1: 1 <= p;

      reconsider p as Real;

      let a,b be Real_Sequence;

      set ap = (a rto_power p);

      set bp = (b rto_power p);

      set ab = ((a + b) rto_power p);

      let n be Nat;

      now

        per cases by A1, XXREAL_0: 1;

          case

           A2: p > 1;

          now

            let n be Nat;

            thus (ap . n) = ( |.(a . n).| to_power p) by Def1;

            thus (bp . n) = ( |.(b . n).| to_power p) by Def1;

            (((a + b) rto_power p) . n) = ( |.((a + b) . n).| to_power p) by Def1

            .= ( |.((a . n) + (b . n)).| to_power p) by SEQ_1: 7;

            hence (ab . n) = ( |.((a . n) + (b . n)).| to_power p);

          end;

          hence thesis by A2, HOLDER_1: 7;

        end;

          case p = 1;

          hence thesis by Lm3;

        end;

      end;

      hence thesis;

    end;



     Lm4: for a,b be Real_Sequence holds for p be Real st 1 = p & (a rto_power p) is summable & (b rto_power p) is summable holds ((a + b) rto_power p) is summable & (( Sum ((a + b) rto_power p)) to_power (1 / p)) <= ((( Sum (a rto_power p)) to_power (1 / p)) + (( Sum (b rto_power p)) to_power (1 / p)))

    proof

      let a,b be Real_Sequence;

      let p be Real such that

       A1: p = 1 and

       A2: (a rto_power p) is summable and

       A3: (b rto_power p) is summable;

       A4:

      now

        let n be Nat;



        thus (((a + b) rto_power p) . n) = ( |.((a + b) . n).| to_power p) by Def1

        .= |.((a + b) . n).| by A1, POWER: 25;



        thus ((a rto_power p) . n) = ( |.(a . n).| to_power p) by Def1

        .= |.(a . n).| by A1, POWER: 25;



        thus ((b rto_power p) . n) = ( |.(b . n).| to_power p) by Def1

        .= |.(b . n).| by A1, POWER: 25;

      end;

      then

       A5: ((a + b) rto_power p) = ( abs (a + b)) by SEQ_1: 12;



       A6: a = ( seq_id a);



       A7: (a rto_power p) = |.a.| by A4, SEQ_1: 12;

      then a is absolutely_summable by A2, SERIES_1:def 4;

      then

      reconsider a1 = a as VECTOR of l1_Space by A6, RSSPACE3: 6;

       |.b.| is summable by A3, A4, SEQ_1: 12;

      then

       A8: ( |.a.| + |.b.|) is summable by A2, A7, SERIES_1: 7;



       A9: (b rto_power p) = |.b.| by A4, SEQ_1: 12;

      then

       A10: (( Sum (b rto_power p)) to_power (1 / p)) = ( Sum |.b.|) by A1, POWER: 25;



       A11: b = ( seq_id b);

      b is absolutely_summable by A3, A9, SERIES_1:def 4;

      then

      reconsider b1 = b as VECTOR of l1_Space by A11, RSSPACE3: 6;



       A12: ||.b1.|| = ( Sum ( abs ( seq_id b1))) by RSSPACE3:def 2, RSSPACE3:def 3;

      deffunc F( Nat) = ( |.(a . $1).| + |.(b . $1).|);

      consider c be Real_Sequence such that

       A14: for n be Nat holds (c . n) = F(n) from SEQ_1:sch 1;

       A15:

      now

        let n be Nat;



         A16: (( abs (a + b)) . n) = |.((a + b) . n).| by SEQ_1: 12;

        hence (( abs (a + b)) . n) >= 0 by COMPLEX1: 46;

        thus (c . n) = ( |.(a . n).| + |.(b . n).|) by A14;

        ( |.(a . n).| + |.(b . n).|) = (( |.a.| . n) + |.(b . n).|) by SEQ_1: 12

        .= (( |.a.| . n) + ( |.b.| . n)) by SEQ_1: 12;

        hence (c . n) = (( |.a.| . n) + ( |.b.| . n)) by A14;

         |.((a + b) . n).| = |.((a . n) + (b . n)).| by SEQ_1: 7;

        then ( |.(a + b).| . n) <= ( |.(a . n).| + |.(b . n).|) by A16, COMPLEX1: 56;

        hence (( abs (a + b)) . n) <= (c . n) by A14;

      end;

      then c = ( |.a.| + |.b.|) by SEQ_1: 7;

      hence ((a + b) rto_power p) is summable by A5, A8, A15, SERIES_1: 20;



       A17: ||.a1.|| = ( Sum ( abs ( seq_id a1))) by RSSPACE3:def 2, RSSPACE3:def 3;



       A19: ||.(a1 + b1).|| = ( Sum ( abs ( seq_id (a1 + b1)))) by RSSPACE3:def 2, RSSPACE3:def 3

      .= ( Sum ( abs ( seq_id (( seq_id a1) + ( seq_id b1))))) by RSSPACE3: 6

      .= ( Sum ( abs (( seq_id a1) + ( seq_id b1))));



       A20: ||.(a1 + b1).|| <= ( ||.a1.|| + ||.b1.||) by RSSPACE3: 7;

      (( Sum (a rto_power p)) to_power (1 / p)) = ( Sum |.a.|) by A1, A7, POWER: 25;

      hence thesis by A1, A5, A10, A20, A19, A17, A12, POWER: 25;

    end;

    theorem :: LP_SPACE:3



     Th3: for a,b be Real_Sequence holds for p be Real st 1 <= p & (a rto_power p) is summable & (b rto_power p) is summable holds ((a + b) rto_power p) is summable & (( Sum ((a + b) rto_power p)) to_power (1 / p)) <= ((( Sum (a rto_power p)) to_power (1 / p)) + (( Sum (b rto_power p)) to_power (1 / p)))

    proof

      let a,b be Real_Sequence;

      let p be Real such that

       A1: 1 <= p and

       A2: (a rto_power p) is summable and

       A3: (b rto_power p) is summable;

      set ab = ((a + b) rto_power p);

      set bp = (b rto_power p);

      set ap = (a rto_power p);

       A4:

      now

        let n be Nat;

        thus (ap . n) = ( |.(a . n).| to_power p) by Def1;

        thus (bp . n) = ( |.(b . n).| to_power p) by Def1;

        (((a + b) rto_power p) . n) = ( |.((a + b) . n).| to_power p) by Def1

        .= ( |.((a . n) + (b . n)).| to_power p) by SEQ_1: 7;

        hence (ab . n) = ( |.((a . n) + (b . n)).| to_power p);

      end;

      reconsider p as Real;

      now

        per cases by A1, XXREAL_0: 1;

          case p > 1;

          hence (( Sum ab) to_power (1 / p)) <= ((( Sum ap) to_power (1 / p)) + (( Sum bp) to_power (1 / p))) & ab is summable by A2, A3, A4, HOLDER_1: 13;

        end;

          case p = 1;

          hence (( Sum ab) to_power (1 / p)) <= ((( Sum ap) to_power (1 / p)) + (( Sum bp) to_power (1 / p))) & ab is summable by A2, A3, Lm4;

        end;

      end;

      hence thesis;

    end;

    theorem :: LP_SPACE:4



     Th4: for p be Real st 1 <= p holds ( the_set_of_RealSequences_l^ p) is linearly-closed

    proof

      let p be Real such that

       A1: p >= 1;

      set W = ( the_set_of_RealSequences_l^ p);



       A2: for v,u be VECTOR of Linear_Space_of_RealSequences st v in ( the_set_of_RealSequences_l^ p) & u in ( the_set_of_RealSequences_l^ p) holds (v + u) in ( the_set_of_RealSequences_l^ p)

      proof

        let v,u be VECTOR of Linear_Space_of_RealSequences such that

         A3: v in W and

         A4: u in W;



         A5: (( seq_id (v + u)) rto_power p) is summable

        proof

          reconsider vq = v as Real_Sequence by FUNCT_2: 66;

          set up = (( seq_id u) rto_power p);

          set vp = (( seq_id v) rto_power p);

          set p1 = (1 / p);

           A7:

          now

            let n be Nat;

            thus

             A8: (vp . n) = ( |.(( seq_id v) . n).| to_power p) by Def1;

            thus

             A9: (up . n) = ( |.(( seq_id u) . n).| to_power p) by Def1;

            thus 0 <= |.(( seq_id v) . n).| by COMPLEX1: 46;

            thus 0 < |.(( seq_id v) . n).| or 0 = |.(( seq_id v) . n).| by COMPLEX1: 46;

            hence 0 <= (vp . n) by A1, A8, POWER: 34, POWER:def 2;

            thus 0 <= |.(( seq_id u) . n).| by COMPLEX1: 46;

            thus 0 < |.(( seq_id u) . n).| or 0 = |.(( seq_id u) . n).| by COMPLEX1: 46;

            hence 0 <= (up . n) by A1, A9, POWER: 34, POWER:def 2;

          end;

          (( seq_id v) rto_power p) is summable by A1, A3, Def2;

          then ( Partial_Sums vp) is bounded_above by A7, SERIES_1: 17;

          then

          consider r be Real such that

           A10: for n be object st n in ( dom ( Partial_Sums vp)) holds (( Partial_Sums vp) . n) < r by SEQ_2:def 1;



           A11: (1 / p) > 0 by A1, XREAL_1: 139;

          reconsider r as Real;



           A12: ( Partial_Sums vp) is non-decreasing by A7, SERIES_1: 16;

          now

            let n be set such that

             A13: n in ( dom ( Partial_Sums vp));

            reconsider n1 = n as Nat by A13;

             0 <= (vp . 0 ) by A7;

            then

             A14: 0 <= (( Partial_Sums vp) . 0 ) by SERIES_1:def 1;

            (( Partial_Sums vp) . 0 ) <= (( Partial_Sums vp) . n1) by A12, SEQM_3: 11;

            hence ((( Partial_Sums vp) . n) to_power p1) < (r to_power p1) by A11, A10, A13, A14, Th1;

          end;

          then

          consider q be Real such that

           A15: for n be set st n in ( dom ( Partial_Sums vp)) holds ((( Partial_Sums vp) . n) to_power p1) < q;

          reconsider uq = u as Real_Sequence by FUNCT_2: 66;



           A17: (( seq_id v) + ( seq_id u)) = ( seq_id (v + u)) by RSSPACE: 2;

          (( seq_id u) rto_power p) is summable by A1, A4, Def2;

          then ( Partial_Sums up) is bounded_above by A7, SERIES_1: 17;

          then

          consider r1 be Real such that

           A18: for n be object st n in ( dom ( Partial_Sums up)) holds (( Partial_Sums up) . n) < r1 by SEQ_2:def 1;

          reconsider r1 as Real;



           A19: ( Partial_Sums up) is non-decreasing by A7, SERIES_1: 16;

          now

            let n be set such that

             A20: n in ( dom ( Partial_Sums up));

            reconsider n1 = n as Nat by A20;

             0 <= (up . 0 ) by A7;

            then

             A21: 0 <= (( Partial_Sums up) . 0 ) by SERIES_1:def 1;

            (( Partial_Sums up) . 0 ) <= (( Partial_Sums up) . n1) by A19, SEQM_3: 11;

            hence ((( Partial_Sums up) . n) to_power p1) < (r1 to_power p1) by A11, A18, A20, A21, Th1;

          end;

          then

          consider q1 be Real such that

           A22: for n be set st n in ( dom ( Partial_Sums up)) holds ((( Partial_Sums up) . n) to_power p1) < q1;

          set g = (q + q1);



           A24: (p * (1 / p)) = ((p * 1) / p) by XCMPLX_1: 74

          .= 1 by A1, XCMPLX_1: 60;

          now

            let n be Nat;



             A25: n in NAT by ORDINAL1:def 12;

             A26:

            now

              assume (( Partial_Sums ((vq + uq) rto_power p)) . n) > 0 ;



              hence (((( Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p) = ((( Partial_Sums ((vq + uq) rto_power p)) . n) to_power ((1 / p) * p)) by POWER: 33

              .= (( Partial_Sums ((vq + uq) rto_power p)) . n) by A24, POWER: 25;

            end;

             NAT = ( dom ( Partial_Sums up)) by SEQ_1: 2;

            then

             A27: ((( Partial_Sums up) . n) to_power p1) < q1 by A22, A25;

             NAT = ( dom ( Partial_Sums vp)) by SEQ_1: 2;

            then

             A28: (((( Partial_Sums up) . n) to_power (1 / p)) + ((( Partial_Sums vp) . n) to_power (1 / p))) < g by A15, A27, XREAL_1: 8, A25;

            ((( Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) <= (((( Partial_Sums up) . n) to_power (1 / p)) + ((( Partial_Sums vp) . n) to_power (1 / p))) by A1, Th2;

            then

             A29: ((( Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) < g by A28, XXREAL_0: 2;

             A30:

            now

              assume

               A31: (( Partial_Sums ((vq + uq) rto_power p)) . n) = 0 ;



              hence (((( Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p) = ( 0 to_power p) by A11, POWER:def 2

              .= (( Partial_Sums ((vq + uq) rto_power p)) . n) by A1, A31, POWER:def 2;

            end;

            now

              let n be Nat;

              thus

               A33: 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| by COMPLEX1: 46;

              (((vq + uq) rto_power p) . n) = ( |.((vq + uq) . n).| to_power p) by Def1;

              hence 0 <= (((vq + uq) rto_power p) . n) by A1, A33, POWER: 34, POWER:def 2;

            end;

            then

             A34: 0 <= (((vq + uq) rto_power p) . 0 );



             A35: (( Partial_Sums ((vq + uq) rto_power p)) . 0 ) <= (( Partial_Sums ((vq + uq) rto_power p)) . n) by A32, SEQM_3: 11, SERIES_1: 16;

            then 0 <= (( Partial_Sums ((vq + uq) rto_power p)) . n) by A34, SERIES_1:def 1;

            then ((( Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) >= 0 by A11, Lm1;

            hence (( Partial_Sums ((vq + uq) rto_power p)) . n) < (g to_power p) by A1, A29, A26, A30, A35, A34, Th1, SERIES_1:def 1;

          end;

          then for n be Nat holds ( Partial_Sums ((vq + uq) rto_power p)) is bounded_above & 0 <= (((vq + uq) rto_power p) . n) by SEQ_2:def 3;

          hence thesis by A17, SERIES_1: 17;

        end;

        thus thesis by A1, A5, Def2;

      end;

      for a be Real holds for v be VECTOR of Linear_Space_of_RealSequences st v in W holds (a * v) in W

      proof

        let a be Real;

        let v be VECTOR of Linear_Space_of_RealSequences such that

         A37: v in W;

        (( seq_id (a * v)) rto_power p) is summable

        proof

          set vp = (( seq_id v) rto_power p);

           A38:

          now

            let n be Nat;

            thus 0 <= |.(( seq_id v) . n).| by COMPLEX1: 46;

            thus

             A39: 0 < |.(( seq_id v) . n).| or 0 = |.(( seq_id v) . n).| by COMPLEX1: 46;

            (vp . n) = ( |.(( seq_id v) . n).| to_power p) by Def1;

            hence 0 <= (vp . n) by A1, A39, POWER: 34, POWER:def 2;

          end;

          vp is summable by A1, A37, Def2;

          then ( Partial_Sums vp) is bounded_above by A38, SERIES_1: 17;

          then

          consider r be Real such that

           A40: for n be object st n in ( dom ( Partial_Sums (( seq_id v) rto_power p))) holds (( Partial_Sums vp) . n) < r by SEQ_2:def 1;



           A41: ( seq_id (a * v)) = (a (#) ( seq_id v)) by RSSPACE: 3;



           A42: for n be Nat holds (( Partial_Sums (( seq_id (a * v)) rto_power p)) . n) = (( |.a.| to_power p) * (( Partial_Sums (( seq_id v) rto_power p)) . n))

          proof

            let n be Nat;

            now

              let n be Nat;



               A43: |.a.| >= 0 by COMPLEX1: 46;



               A44: |.(( seq_id v) . n).| >= 0 by COMPLEX1: 46;



               A45: ((a (#) ( seq_id v)) . n) = (a * (( seq_id v) . n)) by SEQ_1: 9;

              (((a (#) ( seq_id v)) rto_power p) . n) = ( |.((a (#) ( seq_id v)) . n).| to_power p) by Def1

              .= (( |.a.| * |.(( seq_id v) . n).|) to_power p) by A45, COMPLEX1: 65

              .= (( |.a.| to_power p) * ( |.(( seq_id v) . n).| to_power p)) by A1, A43, A44, Lm2;



              hence ((( seq_id (a * v)) rto_power p) . n) = (( |.a.| to_power p) * ((( seq_id v) rto_power p) . n)) by A41, Def1

              .= ((( |.a.| to_power p) (#) (( seq_id v) rto_power p)) . n) by SEQ_1: 9;

            end;

            then for n be object st n in NAT holds ((( seq_id (a * v)) rto_power p) . n) = ((( |.a.| to_power p) (#) (( seq_id v) rto_power p)) . n);

            then

             A46: (( seq_id (a * v)) rto_power p) = (( |.a.| to_power p) (#) (( seq_id v) rto_power p)) by FUNCT_2: 12;

            ( Partial_Sums (( |.a.| to_power p) (#) (( seq_id v) rto_power p))) = (( |.a.| to_power p) (#) ( Partial_Sums (( seq_id v) rto_power p))) by SERIES_1: 9;

            hence thesis by A46, SEQ_1: 9;

          end;



           A47: 0 < ( |.a.| to_power p) or 0 = ( |.a.| to_power p) by A1, Lm1, COMPLEX1: 46;

           A48:

          now

            let n be set such that

             A49: n in ( dom ( Partial_Sums (( seq_id v) rto_power p)));

            ( dom ( Partial_Sums (( seq_id v) rto_power p))) = NAT by SEQ_1: 1;

            hence n in ( dom ( Partial_Sums (( seq_id (a * v)) rto_power p))) by A49, SEQ_1: 1;

            thus (( |.a.| to_power p) * (( Partial_Sums (( seq_id v) rto_power p)) . n)) < (( |.a.| to_power p) * r) or (( |.a.| to_power p) * (( Partial_Sums (( seq_id v) rto_power p)) . n)) = (( |.a.| to_power p) * r) by A40, A47, A49, XREAL_1: 68;

          end;



           A50: for n be set st n in ( dom ( Partial_Sums (( seq_id (a * v)) rto_power p))) holds (( Partial_Sums (( seq_id (a * v)) rto_power p)) . n) < (( |.a.| to_power p) * r) or (( Partial_Sums (( seq_id (a * v)) rto_power p)) . n) = (( |.a.| to_power p) * r)

          proof

            let n be set such that

             A51: n in ( dom ( Partial_Sums (( seq_id (a * v)) rto_power p)));

            reconsider n1 = n as Nat by A51;

            n in NAT by A51, SEQ_1: 1;

            then n in ( dom ( Partial_Sums (( seq_id v) rto_power p))) by SEQ_1: 1;

            then (( |.a.| to_power p) * (( Partial_Sums (( seq_id v) rto_power p)) . n)) < (( |.a.| to_power p) * r) or (( |.a.| to_power p) * (( Partial_Sums (( seq_id v) rto_power p)) . n)) = (( |.a.| to_power p) * r) by A48;

            then (( Partial_Sums (( seq_id (a * v)) rto_power p)) . n1) < (( |.a.| to_power p) * r) or (( Partial_Sums (( seq_id (a * v)) rto_power p)) . n1) = (( |.a.| to_power p) * r) by A42;

            hence thesis;

          end;

          ex r1 be Real st for n be object st n in ( dom ( Partial_Sums (( seq_id (a * v)) rto_power p))) holds (( Partial_Sums (( seq_id (a * v)) rto_power p)) . n) < r1

          proof

            take r1 = ((( |.a.| to_power p) * r) + 1);

            reconsider r1 as Real;

            for n be object st n in ( dom ( Partial_Sums (( seq_id (a * v)) rto_power p))) holds (( Partial_Sums (( seq_id (a * v)) rto_power p)) . n) < r1

            proof



               A52: (( |.a.| to_power p) * r) < ((( |.a.| to_power p) * r) + 1) by XREAL_1: 29;

              let n be object;

              assume n in ( dom ( Partial_Sums (( seq_id (a * v)) rto_power p)));

              hence thesis by A50, A52, XXREAL_0: 2;

            end;

            hence thesis;

          end;

          then

           A53: ( Partial_Sums (( seq_id (a * v)) rto_power p)) is bounded_above by SEQ_2:def 1;

          for n be Nat holds ((( seq_id (a * v)) rto_power p) . n) >= 0

          proof

            set b = (a (#) ( seq_id v));

            let n be Nat;

            ((a (#) ( seq_id v)) . n) = (a * (( seq_id v) . n)) by SEQ_1: 9;

            then ((b rto_power p) . n) = ( |.(a * (( seq_id v) . n)).| to_power p) by Def1;

            hence thesis by A1, A41, Lm1, COMPLEX1: 46;

          end;

          hence thesis by A53, SERIES_1: 17;

        end;

        hence thesis by A1, Def2;

      end;

      hence thesis by A2, RLSUB_1:def 1;

    end;

    theorem :: LP_SPACE:5



     Th5: for p be Real st 1 <= p holds RLSStruct (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )) #) is Subspace of Linear_Space_of_RealSequences

    proof

      let p be Real;

      assume 1 <= p;

      then ( the_set_of_RealSequences_l^ p) is linearly-closed by Th4;

      hence thesis by RSSPACE: 11;

    end;

    theorem :: LP_SPACE:6

    for p be Real st 1 <= p holds RLSStruct (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )) #) is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital by Th5;

    theorem :: LP_SPACE:7

    for p be Real st 1 <= p holds RLSStruct (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )) #) is RealLinearSpace by Th5;

    definition

      let p be Real;

      :: LP_SPACE:def3

      func l_norm^ p -> Function of ( the_set_of_RealSequences_l^ p), REAL means

      : Def3: for x be object st x in ( the_set_of_RealSequences_l^ p) holds (it . x) = (( Sum (( seq_id x) rto_power p)) to_power (1 / p));

      existence

      proof

        deffunc F( object) = (( Sum (( seq_id $1) rto_power p)) to_power (1 / p));



         A1: for z be object st z in ( the_set_of_RealSequences_l^ p) holds F(z) in REAL by XREAL_0:def 1;

        ex f be Function of ( the_set_of_RealSequences_l^ p), REAL st for x be object st x in ( the_set_of_RealSequences_l^ p) holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let NORM1,NORM2 be Function of ( the_set_of_RealSequences_l^ p), REAL such that

         A2: for x be object st x in ( the_set_of_RealSequences_l^ p) holds (NORM1 . x) = (( Sum (( seq_id x) rto_power p)) to_power (1 / p)) and

         A3: for x be object st x in ( the_set_of_RealSequences_l^ p) holds (NORM2 . x) = (( Sum (( seq_id x) rto_power p)) to_power (1 / p));



         A4: for z be object st z in ( the_set_of_RealSequences_l^ p) holds (NORM1 . z) = (NORM2 . z)

        proof

          let z be object such that

           A5: z in ( the_set_of_RealSequences_l^ p);

          (NORM1 . z) = (( Sum (( seq_id z) rto_power p)) to_power (1 / p)) by A2, A5;

          hence thesis by A3, A5;

        end;



         A6: ( dom NORM2) = ( the_set_of_RealSequences_l^ p) by FUNCT_2:def 1;

        ( dom NORM1) = ( the_set_of_RealSequences_l^ p) by FUNCT_2:def 1;

        hence thesis by A6, A4, FUNCT_1: 2;

      end;

    end

    theorem :: LP_SPACE:8



     Th8: for p be Real st 1 <= p holds NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) is RealLinearSpace

    proof

      let p be Real;

      assume 1 <= p;

      then RLSStruct (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )) #) is RealLinearSpace by Th5;

      hence thesis by RSSPACE3: 2;

    end;

    theorem :: LP_SPACE:9



     Th9: for p be Real st p >= 1 holds NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) is Subspace of Linear_Space_of_RealSequences

    proof

      set V = Linear_Space_of_RealSequences ;

      let p be Real such that

       A1: 1 <= p;

      set lSpacep = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      reconsider lSpacep as RealLinearSpace by A1, Th8;

      set w1 = the RLSStruct of lSpacep;



       A2: w1 is Subspace of V by A1, Th5;

      then

       A3: the Mult of lSpacep = (the Mult of V | [: REAL , the carrier of lSpacep:]) by RLSUB_1:def 2;

      ( 0. w1) = ( 0. V) by A2, RLSUB_1:def 2;

      then

       A4: ( 0. lSpacep) = ( 0. V);

      the addF of lSpacep = (the addF of V || the carrier of lSpacep) by A2, RLSUB_1:def 2;

      hence thesis by A4, A3, RLSUB_1:def 2;

    end;

    begin

    theorem :: LP_SPACE:10



     Th10: for p be Real st 1 <= p holds for lp be non empty NORMSTR st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds the carrier of lp = ( the_set_of_RealSequences_l^ p) & (for x be set holds x is VECTOR of lp iff x is Real_Sequence & (( seq_id x) rto_power p) is summable) & ( 0. lp) = Zeroseq & (for x be VECTOR of lp holds x = ( seq_id x)) & (for x,y be VECTOR of lp holds (x + y) = (( seq_id x) + ( seq_id y))) & (for r be Real holds for x be VECTOR of lp holds (r * x) = (r (#) ( seq_id x))) & (for x be VECTOR of lp holds ( - x) = ( - ( seq_id x)) & ( seq_id ( - x)) = ( - ( seq_id x))) & (for x,y be VECTOR of lp holds (x - y) = (( seq_id x) - ( seq_id y))) & (for x be VECTOR of lp holds (( seq_id x) rto_power p) is summable) & for x be VECTOR of lp holds ||.x.|| = (( Sum (( seq_id x) rto_power p)) to_power (1 / p))

    proof

      let p be Real such that

       A1: 1 <= p;

      let lp be non empty NORMSTR such that

       A2: lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);



       A3: for x be VECTOR of lp holds ||.x.|| = (( Sum (( seq_id x) rto_power p)) to_power (1 / p)) by A2, Def3;



       A4: for x,y be VECTOR of lp holds (x + y) = (( seq_id x) + ( seq_id y))

      proof

        let x,y be VECTOR of lp;



         A5: lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

        then

        reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1: 10;

        reconsider y1 = y as VECTOR of Linear_Space_of_RealSequences by A5, RLSUB_1: 10;

        set L1 = Linear_Space_of_RealSequences ;

        set W = ( the_set_of_RealSequences_l^ p);

        ( dom the addF of L1) = [:the carrier of L1, the carrier of L1:] by FUNCT_2:def 1;

        then

         A6: ( dom (the addF of Linear_Space_of_RealSequences || W)) = [:W, W:] by RELAT_1: 62;

        W is linearly-closed by A1, Th4;



        then (x + y) = ((the addF of Linear_Space_of_RealSequences || W) . [x, y]) by A2, RSSPACE:def 8

        .= (x1 + y1) by A2, A6, FUNCT_1: 47;

        hence thesis by RSSPACE: 2;

      end;



       A7: for r be Real holds for x be VECTOR of lp holds (r * x) = (r (#) ( seq_id x))

      proof

        set W = ( the_set_of_RealSequences_l^ p);

        set L1 = Linear_Space_of_RealSequences ;

        let r be Real;

        reconsider r as Element of REAL by XREAL_0:def 1;

        let x be VECTOR of lp;

        ( dom the Mult of L1) = [: REAL , the carrier of L1:] by FUNCT_2:def 1;

        then

         A8: ( dom (the Mult of Linear_Space_of_RealSequences | [: REAL , W:])) = [: REAL , W:] by RELAT_1: 62, ZFMISC_1: 96;

        lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

        then

        reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1: 10;

        W is linearly-closed by A1, Th4;



        then (r * x) = ((the Mult of Linear_Space_of_RealSequences | [: REAL , W:]) . [r, x]) by A2, RSSPACE:def 9

        .= (r * x1) by A2, A8, FUNCT_1: 47;

        hence thesis by RSSPACE: 3;

      end;

      ( the_set_of_RealSequences_l^ p) is linearly-closed by A1, Th4;



      then

       A9: ( 0. lp) = ( 0. Linear_Space_of_RealSequences ) by A2, RSSPACE:def 10

      .= Zeroseq ;



       A10: for x be set holds x is Element of lp iff x is Real_Sequence & (( seq_id x) rto_power p) is summable

      proof

        let x be set;

        x in ( the_set_of_RealSequences_l^ p) iff (( seq_id x) rto_power p) is summable & x in the_set_of_RealSequences by A1, Def2;

        hence thesis by A2, FUNCT_2: 8, FUNCT_2: 66;

      end;



       A11: for x be set holds x is VECTOR of lp implies x = ( seq_id x)

      proof

        let x be set;

        x in the_set_of_RealSequences iff x is Real_Sequence by FUNCT_2: 8, FUNCT_2: 66;

        hence thesis by A1, A2, Def2;

      end;



       A12: for x be VECTOR of lp holds ( - x) = ( - ( seq_id x)) & ( seq_id ( - x)) = ( - ( seq_id x))

      proof

        let x be VECTOR of lp;

        lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;



        then ( - x) = (( - 1) * x) by RLVECT_1: 16

        .= ( - ( seq_id x)) by A7;

        hence thesis;

      end;

      for x,y be VECTOR of lp holds (x - y) = (( seq_id x) - ( seq_id y))

      proof

        let x,y be VECTOR of lp;



        thus (x - y) = (( seq_id x) + ( seq_id ( - y))) by A4

        .= (( seq_id x) - ( seq_id y)) by A12;

      end;

      hence thesis by A2, A10, A11, A9, A4, A7, A12, A3;

    end;

    theorem :: LP_SPACE:11



     Th11: for p be Real st p >= 1 holds for rseq be Real_Sequence st (for n be Nat holds (rseq . n) = 0 ) holds (rseq rto_power p) is summable & (( Sum (rseq rto_power p)) to_power (1 / p)) = 0

    proof

      let p be Real such that

       A1: p >= 1;



       A2: (1 / p) > 0 by A1, XREAL_1: 139;

      let rseq be Real_Sequence such that

       A3: for n be Nat holds (rseq . n) = 0 ;



       A4: for n be Nat holds ((rseq rto_power p) . n) = 0

      proof

        let n be Nat;

        (rseq . n) = 0 by A3;

        then |.(rseq . n).| = 0 by ABSVALUE: 2;

        then ( |.(rseq . n).| to_power p) = 0 by A1, POWER:def 2;

        hence thesis by Def1;

      end;



       A5: for m be Nat holds (( Partial_Sums (rseq rto_power p)) . m) = 0

      proof

        defpred P[ Nat] means ((rseq rto_power p) . $1) = (( Partial_Sums (rseq rto_power p)) . $1);

        let m be Nat;



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

        proof

          let k be Nat such that

           A7: ((rseq rto_power p) . k) = (( Partial_Sums (rseq rto_power p)) . k);



          thus ((rseq rto_power p) . (k + 1)) = ( 0 + ((rseq rto_power p) . (k + 1)))

          .= (((rseq rto_power p) . k) + ((rseq rto_power p) . (k + 1))) by A4

          .= (( Partial_Sums (rseq rto_power p)) . (k + 1)) by A7, SERIES_1:def 1;

        end;



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

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



        hence (( Partial_Sums (rseq rto_power p)) . m) = ((rseq rto_power p) . m)

        .= 0 by A4;

      end;



       A9: for e be Real st 0 < e holds ex n be Nat st for m be Nat st n <= m holds |.((( Partial_Sums (rseq rto_power p)) . m) - 0 ).| < e

      proof

        let e be Real such that

         A10: 0 < e;

        take 0 ;

        let m be Nat such that 0 <= m;

         |.((( Partial_Sums (rseq rto_power p)) . m) - 0 ).| = |.( 0 - 0 ).| by A5

        .= 0 by ABSVALUE:def 1;

        hence thesis by A10;

      end;

      then

       A11: ( Partial_Sums (rseq rto_power p)) is convergent by SEQ_2:def 6;

      then ( lim ( Partial_Sums (rseq rto_power p))) = 0 by A9, SEQ_2:def 7;

      then ( Sum (rseq rto_power p)) = 0 by SERIES_1:def 3;

      hence thesis by A2, A11, POWER:def 2, SERIES_1:def 2;

    end;

    theorem :: LP_SPACE:12



     Th12: for p be Real st 1 <= p holds for rseq be Real_Sequence st (rseq rto_power p) is summable & (( Sum (rseq rto_power p)) to_power (1 / p)) = 0 holds for n be Nat holds (rseq . n) = 0

    proof

      let p be Real such that

       A1: 1 <= p;



       A2: (1 / p) > 0 by A1, XREAL_1: 139;

      let rseq be Real_Sequence such that

       A3: (rseq rto_power p) is summable and

       A4: (( Sum (rseq rto_power p)) to_power (1 / p)) = 0 ;



       A5: for i be Nat holds ((rseq rto_power p) . i) >= 0

      proof

        let i be Nat;

        ((rseq rto_power p) . i) = ( |.(rseq . i).| to_power p) by Def1;

        hence thesis by A1, Lm1, COMPLEX1: 46;

      end;



      then ((( Sum (rseq rto_power p)) to_power (1 / p)) to_power p) = (( Sum (rseq rto_power p)) to_power ((1 / p) * p)) by A1, A2, A3, HOLDER_1: 2, SERIES_1: 18

      .= (( Sum (rseq rto_power p)) to_power 1) by A1, XCMPLX_1: 106

      .= ( Sum (rseq rto_power p)) by POWER: 25;

      then

       A6: ( Sum (rseq rto_power p)) = 0 by A1, A4, POWER:def 2;

      now

        let n be Nat;

        reconsider n9 = n as Nat;



         A7: ( 0 to_power (1 / p)) = 0 by A2, POWER:def 2;

        ((rseq rto_power p) . n9) = ( |.(rseq . n9).| to_power p) by Def1;

        then

         A8: ( |.(rseq . n).| to_power p) = 0 by A3, A5, A6, RSSPACE: 17;

        (( |.(rseq . n).| to_power p) to_power (1 / p)) = ( |.(rseq . n).| to_power (p * (1 / p))) by A1, A2, COMPLEX1: 46, HOLDER_1: 2

        .= ( |.(rseq . n).| to_power 1) by A1, XCMPLX_1: 106

        .= |.(rseq . n).| by POWER: 25;

        hence (rseq . n) = 0 by A8, A7, ABSVALUE: 2;

      end;

      hence thesis;

    end;



     Lm5: for p be Real st 1 <= p holds for lp be non empty NORMSTR st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds for x be Point of lp, a be Real holds (( seq_id (a * x)) rto_power p) = (( |.a.| to_power p) (#) (( seq_id x) rto_power p))

    proof

      let p be Real such that

       A1: 1 <= p;

      let lp be non empty NORMSTR such that

       A2: lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      let x be Point of lp;

      let a be Real;

      now

        let n1 be object;

        assume n1 in NAT ;

        then

        reconsider n = n1 as Nat;



         A3: |.a.| >= 0 by COMPLEX1: 46;



         A4: |.(( seq_id x) . n).| >= 0 by COMPLEX1: 46;

        ((( seq_id (a * x)) rto_power p) . n) = ( |.(( seq_id (a * x)) . n).| to_power p) by Def1

        .= ( |.(( seq_id (a (#) ( seq_id x))) . n).| to_power p) by A1, A2, Th10

        .= ( |.(a * (( seq_id x) . n)).| to_power p) by SEQ_1: 9

        .= (( |.a.| * |.(( seq_id x) . n).|) to_power p) by COMPLEX1: 65

        .= (( |.a.| to_power p) * ( |.(( seq_id x) . n).| to_power p)) by A1, A3, A4, Lm2

        .= (( |.a.| to_power p) * ((( seq_id x) rto_power p) . n)) by Def1

        .= ((( |.a.| to_power p) (#) (( seq_id x) rto_power p)) . n) by SEQ_1: 9;

        hence ((( seq_id (a * x)) rto_power p) . n1) = ((( |.a.| to_power p) (#) (( seq_id x) rto_power p)) . n1);

      end;

      hence thesis by FUNCT_2: 12;

    end;



     Lm6: for p be Real st 1 <= p holds for lp be non empty NORMSTR st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds for x be Point of lp, a be Real holds ( Sum (( seq_id (a * x)) rto_power p)) = (( |.a.| to_power p) * ( Sum (( seq_id x) rto_power p)))

    proof

      let p be Real such that

       A1: 1 <= p;

      let lp be non empty NORMSTR such that

       A2: lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      let x be Point of lp;



       A3: (( seq_id x) rto_power p) is summable by A1, A2, Th10;

      let a be Real;



      thus ( Sum (( seq_id (a * x)) rto_power p)) = ( Sum (( |.a.| to_power p) (#) (( seq_id x) rto_power p))) by A1, A2, Lm5

      .= (( |.a.| to_power p) * ( Sum (( seq_id x) rto_power p))) by A3, SERIES_1: 10;

    end;



     Lm7: for p be Real st 1 <= p holds for lp be non empty NORMSTR st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds for x be Point of lp, a be Real holds (( Sum (( seq_id (a * x)) rto_power p)) to_power (1 / p)) = ( |.a.| * (( Sum (( seq_id x) rto_power p)) to_power (1 / p)))

    proof

      let p be Real such that

       A1: 1 <= p;



       A2: (1 / p) > 0 by A1, XREAL_1: 139;

      let lp be non empty NORMSTR such that

       A3: lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      let x be Point of lp;

       A4:

      now

        let n be Nat;

        ((( seq_id x) rto_power p) . n) = ( |.(( seq_id x) . n).| to_power p) by Def1;

        hence ((( seq_id x) rto_power p) . n) >= 0 by A1, Lm1, COMPLEX1: 46;

      end;

      (( seq_id x) rto_power p) is summable by A1, A3, Th10;

      then

       A5: 0 <= ( Sum (( seq_id x) rto_power p)) by A4, SERIES_1: 18;

      let a be Real;



       A6: ( |.a.| to_power p) >= 0 by A1, Lm1, COMPLEX1: 46;



      thus (( Sum (( seq_id (a * x)) rto_power p)) to_power (1 / p)) = ((( |.a.| to_power p) * ( Sum (( seq_id x) rto_power p))) to_power (1 / p)) by A1, A3, Lm6

      .= ((( |.a.| to_power p) to_power (1 / p)) * (( Sum (( seq_id x) rto_power p)) to_power (1 / p))) by A2, A5, A6, Lm2

      .= (( |.a.| to_power (p * (1 / p))) * (( Sum (( seq_id x) rto_power p)) to_power (1 / p))) by A1, A2, COMPLEX1: 46, HOLDER_1: 2

      .= (( |.a.| to_power 1) * (( Sum (( seq_id x) rto_power p)) to_power (1 / p))) by A1, XCMPLX_1: 106

      .= ( |.a.| * (( Sum (( seq_id x) rto_power p)) to_power (1 / p))) by POWER: 25;

    end;

    theorem :: LP_SPACE:13



     Th13: for p be Real st 1 <= p holds for lp be non empty NORMSTR st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds for x,y be Point of lp, a be Real holds ( ||.x.|| = 0 iff x = ( 0. lp)) & 0 <= ||.x.|| & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(a * x).|| = ( |.a.| * ||.x.||)

    proof

      let p be Real such that

       A1: 1 <= p;



       A2: (1 / p) > 0 by A1, XREAL_1: 139;

      let lp be non empty NORMSTR such that

       A3: lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      let x,y be Point of lp;



       A4: (( seq_id y) rto_power p) is summable by A1, A3, Th10;



       A5: ||.y.|| = (( Sum (( seq_id y) rto_power p)) to_power (1 / p)) by A3, Def3;



       A6: ||.x.|| = (( Sum (( seq_id x) rto_power p)) to_power (1 / p)) by A3, Def3;

       A7:

      now



         A8: ||.x.|| = (( Sum (( seq_id x) rto_power p)) to_power (1 / p)) by A3, Def3;



         A9: x in the_set_of_RealSequences by A1, A3, Def2;

        assume

         A10: ||.x.|| = 0 ;

        (( seq_id x) rto_power p) is summable by A1, A3, Th10;

        then for n be Nat holds 0 = (( seq_id x) . n) by A1, A10, A8, Th12;



        hence x = Zeroseq by A9, RSSPACE: 5

        .= ( 0. lp) by A1, A3, Th10;

      end;



       A11: (( seq_id x) rto_power p) is summable by A1, A3, Def2;



       A12: (( Sum (( seq_id x) rto_power p)) to_power (1 / p)) = ||.x.|| by A3, Def3;

       A13:

      now

        assume x = ( 0. lp);

        then x = Zeroseq by A1, A3, Th10;

        then

         A14: for n be Nat holds (( seq_id x) . n) = 0 by RSSPACE: 4;



        thus ||.x.|| = (( Sum (( seq_id x) rto_power p)) to_power (1 / p)) by A3, Def3

        .= 0 by A1, A14, Th11;

      end;

      let a be Real;



       A15: for n be Nat holds 0 <= ((( seq_id x) rto_power p) . n)

      proof

        set xp = (( seq_id x) rto_power p);

        let n be Nat;



         A16: 0 < |.(( seq_id x) . n).| or 0 = |.(( seq_id x) . n).| by COMPLEX1: 46;

        (xp . n) = ( |.(( seq_id x) . n).| to_power p) by Def1;

        hence thesis by A1, A16, POWER: 34, POWER:def 2;

      end;

      (( seq_id x) + ( seq_id y)) = ( seq_id (( seq_id x) + ( seq_id y)))

      .= ( seq_id (x + y)) by A1, A3, Th10;

      then

       A17: (( Sum ((( seq_id x) + ( seq_id y)) rto_power p)) to_power (1 / p)) = ||.(x + y).|| by A3, Def3;

      (( seq_id x) rto_power p) is summable by A1, A3, Th10;

      then

       A18: ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by A1, A6, A5, A17, A4, Th3;



       A19: ||.x.|| = (( Sum (( seq_id x) rto_power p)) to_power (1 / p)) by A3, Def3;

       ||.(a * x).|| = (( Sum (( seq_id (a * x)) rto_power p)) to_power (1 / p)) by A3, Def3

      .= ( |.a.| * ||.x.||) by A1, A3, A19, Lm7;

      hence thesis by A2, A7, A13, A15, A11, A12, A18, Lm1, SERIES_1: 18;

    end;

    theorem :: LP_SPACE:14



     Th14: for p be Real st p >= 1 holds for lp be non empty NORMSTR st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds lp is reflexive discerning RealNormSpace-like

    proof

      let p be Real such that

       A1: p >= 1;

      let lp be non empty NORMSTR;

      assume

       A2: lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      hence ||.( 0. lp).|| = 0 by A1, Th13;

      for x,y be Point of lp, a be Real holds ( ||.x.|| = 0 iff x = ( 0. lp)) & 0 <= ||.x.|| & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(a * x).|| = ( |.a.| * ||.x.||) by A1, Th13, A2;

      hence thesis by NORMSP_1:def 1;

    end;

    theorem :: LP_SPACE:15

    for p be Real st p >= 1 holds for lp be non empty NORMSTR st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds lp is RealNormSpace by Th9, Th14;



     Lm8: for p be Real st 0 < p holds for c be Real, seq be Real_Sequence st seq is convergent holds for rseq be Real_Sequence st (for i be Nat holds (rseq . i) = ( |.((seq . i) - c).| to_power p)) holds rseq is convergent & ( lim rseq) = ( |.(( lim seq) - c).| to_power p)

    proof

      let p be Real such that

       A1: 0 < p;

      let c be Real;

      let seq be Real_Sequence such that

       A2: seq is convergent;

      deffunc F( set) = |.((seq . $1) - c).|;

      consider b be Real_Sequence such that

       A3: for n be Nat holds (b . n) = F(n) from SEQ_1:sch 1;

      let rseq be Real_Sequence such that

       A4: for i be Nat holds (rseq . i) = ( |.((seq . i) - c).| to_power p);



       A5: for n be Nat holds (rseq . n) = ((b . n) to_power p)

      proof

        let n be Nat;

        (rseq . n) = ( |.((seq . n) - c).| to_power p) by A4

        .= ((b . n) to_power p) by A3;

        hence thesis;

      end;



       A6: for n be Nat holds 0 <= (b . n)

      proof

        let n be Nat;

        (b . n) = |.((seq . n) - c).| by A3;

        hence thesis by COMPLEX1: 46;

      end;



       A7: ( lim b) = |.(( lim seq) - c).| by A2, A3, RSSPACE3: 1;

      b is convergent by A2, A3, RSSPACE3: 1;

      hence thesis by A1, A7, A6, A5, HOLDER_1: 10;

    end;



     Lm9: for p be Real st 0 < p holds for c be Real, seq,seq1 be Real_Sequence st seq is convergent & seq1 is convergent holds for rseq be Real_Sequence st (for i be Nat holds (rseq . i) = (( |.((seq . i) - c).| to_power p) + (seq1 . i))) holds rseq is convergent & ( lim rseq) = (( |.(( lim seq) - c).| to_power p) + ( lim seq1))

    proof

      let p be Real such that

       A1: 0 < p;

      let c be Real;

      let seq,seq1 be Real_Sequence such that

       A2: seq is convergent and

       A3: seq1 is convergent;

      deffunc F( set) = ( |.((seq . $1) - c).| to_power p);

      consider b be Real_Sequence such that

       A4: for n be Nat holds (b . n) = F(n) from SEQ_1:sch 1;

      let rseq be Real_Sequence such that

       A5: for i be Nat holds (rseq . i) = (( |.((seq . i) - c).| to_power p) + (seq1 . i));

      now

        let n be Nat;



        thus (rseq . n) = (( |.((seq . n) - c).| to_power p) + (seq1 . n)) by A5

        .= ((b . n) + (seq1 . n)) by A4;

      end;

      then

       A6: rseq = (b + seq1) by SEQ_1: 7;



       A7: b is convergent by A1, A2, A4, Lm8;

      hence rseq is convergent by A3, A6, SEQ_2: 5;

      ( lim b) = ( |.(( lim seq) - c).| to_power p) by A1, A2, A4, Lm8;

      hence thesis by A3, A7, A6, SEQ_2: 6;

    end;



     Lm10: for a,b be Real_Sequence holds a = ((a + b) - b)

    proof

      let a,b be Real_Sequence;

      now

        let n be Element of NAT ;

        ((a + (b + ( - b))) . n) = ((a . n) + ((b + ( - b)) . n)) by SEQ_1: 7

        .= ((a . n) + ((b . n) + (( - b) . n))) by SEQ_1: 7

        .= ((a . n) + ((b . n) + ( - (b . n)))) by SEQ_1: 10

        .= (a . n);

        hence (((a + b) - b) . n) = (a . n) by SEQ_1: 13;

      end;

      hence thesis by FUNCT_2: 63;

    end;



     Lm11: for p be Real st p >= 1 holds for a,b be Real_Sequence st (a rto_power p) is summable & (b rto_power p) is summable holds ((a + b) rto_power p) is summable

    proof

      let p be Real such that

       A1: p >= 1;

      let a,b be Real_Sequence such that

       A2: (a rto_power p) is summable and

       A3: (b rto_power p) is summable;

      reconsider a1 = a, b1 = b as set;



       A4: a1 in the_set_of_RealSequences by FUNCT_2: 8;

      ( seq_id a1) = a;

      then

       A6: a1 in ( the_set_of_RealSequences_l^ p) by A1, A2, A4, Def2;



       A7: b1 in the_set_of_RealSequences by FUNCT_2: 8;

      ( seq_id b1) = b;

      then

       A9: b1 in ( the_set_of_RealSequences_l^ p) by A1, A3, A7, Def2;

      then

      reconsider b1 as VECTOR of Linear_Space_of_RealSequences ;

      reconsider a1 as VECTOR of Linear_Space_of_RealSequences by A6;



       A10: ( seq_id (a1 + b1)) = ( seq_id (( seq_id a1) + ( seq_id b1))) by RSSPACE: 2

      .= (a + b);

      ( the_set_of_RealSequences_l^ p) is linearly-closed by A1, Th4;

      then (a1 + b1) in ( the_set_of_RealSequences_l^ p) by A6, A9, RLSUB_1:def 1;

      hence thesis by A1, A10, Def2;

    end;

    theorem :: LP_SPACE:16



     Th16: for p be Real st 1 <= p holds for lp be RealNormSpace st lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #) holds for vseq be sequence of lp st vseq is Cauchy_sequence_by_Norm holds vseq is convergent

    proof

      let p be Real such that

       A1: 1 <= p;



       A2: (1 / p) > 0 by A1, XREAL_1: 139;

      let lp be RealNormSpace such that

       A3: lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      let vseq be sequence of lp such that

       A4: vseq is Cauchy_sequence_by_Norm;

      defpred P[ object, object] means ex i be Nat st $1 = i & ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i)) & rseqi is convergent & $2 = ( lim rseqi);



       A5: (p * (1 / p)) = ((p * 1) / p) by XCMPLX_1: 74

      .= 1 by A1, XCMPLX_1: 60;



       A6: for x be object st x in NAT holds ex y be object st y in REAL & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Nat;

        deffunc F( Nat) = (( seq_id (vseq . $1)) . i);

        consider rseqi be Real_Sequence such that

         A7: for n be Nat holds (rseqi . n) = F(n) from SEQ_1:sch 1;

        reconsider lr = ( lim rseqi) as Element of REAL by XREAL_0:def 1;

        take lr;

        now

          let e1 be Real such that

           A8: e1 > 0 ;

          reconsider e = e1 as Real;

          thus ex k be Nat st for m be Nat st k <= m holds |.((rseqi . m) - (rseqi . k)).| < e1

          proof

            consider k be Nat such that

             A9: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A4, A8, RSSPACE3: 8;

            for m be Nat st k <= m holds |.((rseqi . m) - (rseqi . k)).| < e

            proof

              let m be Nat such that

               A10: k <= m;



               A11: ||.((vseq . m) - (vseq . k)).|| = (( Sum (( seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) by A3, Def3;

              then (( Sum (( seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) < e by A9, A10;

              then

               A12: ((( Sum (( seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) to_power p) < (e to_power p) by A1, A11, Th1, NORMSP_1: 4;

               A13:

              now

                let i be Nat;

                ((( seq_id ((vseq . m) - (vseq . k))) rto_power p) . i) = ( |.(( seq_id ((vseq . m) - (vseq . k))) . i).| to_power p) by Def1;

                hence ((( seq_id ((vseq . m) - (vseq . k))) rto_power p) . i) >= 0 by A1, Lm1, COMPLEX1: 46;

              end;

              reconsider vsem = (vseq . m), vsek = (vseq . k) as VECTOR of lp;

               A14:

              now

                let a,b,c be Real such that

                 A15: a = 0 and

                 A16: b > 0 and

                 A17: c > 0 ;

                (b * c) > 0 by A16, A17, XREAL_1: 129;

                hence (a to_power (b * c)) = 0 by A15, POWER:def 2;

              end;

               A18:

              now

                let a,b,c be Real such that

                 A19: a = 0 and

                 A20: b > 0 and

                 A21: c > 0 ;

                (a to_power b) = 0 by A19, A20, POWER:def 2;

                hence ((a to_power b) to_power c) = 0 by A21, POWER:def 2;

              end;

               A22:

              now

                let a,b,c be Real such that

                 A23: a = 0 and

                 A24: b > 0 and

                 A25: c > 0 ;



                thus ((a to_power b) to_power c) = 0 by A18, A23, A24, A25

                .= (a to_power (b * c)) by A14, A23, A24, A25;

              end;



               A26: for a,b,c be Real st a >= 0 & b > 0 & c > 0 holds ((a to_power b) to_power c) = (a to_power (b * c))

              proof

                let a,b,c be Real such that

                 A27: a >= 0 and

                 A28: b > 0 and

                 A29: c > 0 ;

                a > 0 or a = 0 by A27;

                hence thesis by A22, A28, A29, POWER: 33;

              end;

              ((( seq_id ((vseq . m) - (vseq . k))) rto_power p) . i) = ( |.(( seq_id ((vseq . m) - (vseq . k))) . i).| to_power p) by Def1;



              then

               A30: (((( seq_id ((vseq . m) - (vseq . k))) rto_power p) . i) to_power (1 / p)) = ( |.(( seq_id ((vseq . m) - (vseq . k))) . i).| to_power 1) by A1, A2, A5, A26, COMPLEX1: 46

              .= |.(( seq_id ((vseq . m) - (vseq . k))) . i).| by POWER: 25;



               A31: (rseqi . m) = (( seq_id (vseq . m)) . i) by A7;



               A32: (( seq_id ((vseq . m) - (vseq . k))) rto_power p) is summable by A1, A3, Th10;

              then

               A33: ((( seq_id ((vseq . m) - (vseq . k))) rto_power p) . i) <= ( Sum (( seq_id ((vseq . m) - (vseq . k))) rto_power p)) by A13, RSSPACE2: 3;

              ((( Sum (( seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) to_power p) = (( Sum (( seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power ((1 / p) * p)) by A1, A2, A32, A13, HOLDER_1: 2, SERIES_1: 18

              .= ( Sum (( seq_id ((vseq . m) - (vseq . k))) rto_power p)) by A5, POWER: 25;

              then

               A34: ((( seq_id ((vseq . m) - (vseq . k))) rto_power p) . i) < (e to_power p) by A12, A33, XXREAL_0: 2;



               A35: (rseqi . k) = (( seq_id (vseq . k)) . i) by A7;

              (vsem - vsek) = (( seq_id vsem) - ( seq_id vsek)) by A1, A3, Th10;



              then

               A36: |.(( seq_id ((vseq . m) - (vseq . k))) . i).| = |.((( seq_id (vseq . m)) . i) + (( - ( seq_id (vseq . k))) . i)).| by SEQ_1: 7

              .= |.((( seq_id (vseq . m)) . i) + ( - (( seq_id (vseq . k)) . i))).| by SEQ_1: 10

              .= |.((rseqi . m) - (rseqi . k)).| by A31, A35;

              ((e to_power p) to_power (1 / p)) = (e to_power ((1 / p) * p)) by A8, POWER: 33

              .= (e to_power 1) by A1, XCMPLX_1: 106

              .= e by POWER: 25;

              hence thesis by A2, A13, A30, A34, A36, Th1;

            end;

            hence thesis;

          end;

        end;

        then rseqi is convergent by SEQ_4: 41;

        hence thesis by A7;

      end;

      consider f be sequence of REAL such that

       A37: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A6);

      reconsider tseq = f as Real_Sequence;

       A38:

      now

        let i be Nat;

        reconsider x = i as set;



         A39: i in NAT by ORDINAL1:def 12;

        ex i0 be Nat st x = i0 & ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i0)) & rseqi is convergent & (f . x) = ( lim rseqi) by A37, A39;

        hence ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i)) & rseqi is convergent & (tseq . i) = ( lim rseqi);

      end;



       A40: for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) < e

      proof



         A41: for n be Nat holds for i be Nat holds for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i)

        proof

          let n be Nat;

          defpred P[ Nat] means for rseq be Real_Sequence st for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . $1) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . $1);



           A42: for m,k be Nat holds ( seq_id ((vseq . m) - (vseq . k))) = (( seq_id (vseq . m)) - ( seq_id (vseq . k)))

          proof

            let m,k be Nat;

            ( seq_id ((vseq . m) - (vseq . k))) = ( seq_id (( seq_id (vseq . m)) - ( seq_id (vseq . k)))) by A1, A3, Th10;

            hence thesis;

          end;

          now

            let i be Nat such that

             A43: for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i);

            thus for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1))) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . (i + 1))

            proof

              deffunc F( Nat) = (( Partial_Sums (( seq_id ((vseq . $1) - (vseq . n))) rto_power p)) . i);

              consider rseqb be Real_Sequence such that

               A44: for m be Nat holds (rseqb . m) = F(m) from SEQ_1:sch 1;

              consider rseq0 be Real_Sequence such that

               A45: for m be Nat holds (rseq0 . m) = (( seq_id (vseq . m)) . (i + 1)) and

               A46: rseq0 is convergent and

               A47: (tseq . (i + 1)) = ( lim rseq0) by A38;

              let rseq be Real_Sequence such that

               A48: for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1));

               A49:

              now

                let m be Nat;



                thus (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1)) by A48

                .= (((( seq_id ((vseq . m) - (vseq . n))) rto_power p) . (i + 1)) + (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i)) by SERIES_1:def 1

                .= ((((( seq_id (vseq . m)) - ( seq_id (vseq . n))) rto_power p) . (i + 1)) + (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i)) by A42

                .= ((((( seq_id (vseq . m)) - ( seq_id (vseq . n))) rto_power p) . (i + 1)) + (rseqb . m)) by A44

                .= (( |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . (i + 1)).| to_power p) + (rseqb . m)) by Def1

                .= (( |.((( seq_id (vseq . m)) . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))).| to_power p) + (rseqb . m)) by SEQ_1: 7

                .= (( |.((( seq_id (vseq . m)) . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1)))).| to_power p) + (rseqb . m)) by SEQ_1: 10

                .= (( |.((( seq_id (vseq . m)) . (i + 1)) - (( seq_id (vseq . n)) . (i + 1))).| to_power p) + (rseqb . m))

                .= (( |.((rseq0 . m) - (( seq_id (vseq . n)) . (i + 1))).| to_power p) + (rseqb . m)) by A45;

              end;



               A50: ( lim rseqb) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i) by A43, A44;



               A51: rseqb is convergent by A43, A44;



              then ( lim rseq) = (( |.(( lim rseq0) - (( seq_id (vseq . n)) . (i + 1))).| to_power p) + ( lim rseqb)) by A1, A46, A49, Lm9

              .= (( |.((tseq . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1)))).| to_power p) + ( lim rseqb)) by A47

              .= (( |.((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))).| to_power p) + ( lim rseqb)) by SEQ_1: 10

              .= (( |.((tseq - ( seq_id (vseq . n))) . (i + 1)).| to_power p) + ( lim rseqb)) by SEQ_1: 7

              .= ((((tseq - ( seq_id (vseq . n))) rto_power p) . (i + 1)) + (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i)) by A50, Def1

              .= (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . (i + 1)) by SERIES_1:def 1;

              hence thesis by A1, A51, A46, A49, Lm9;

            end;

          end;

          then

           A52: for i be Nat st P[i] holds P[(i + 1)];

          now

            let rseq be Real_Sequence such that

             A53: for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 );

            thus rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . 0 )

            proof

              consider rseq0 be Real_Sequence such that

               A54: for m be Nat holds (rseq0 . m) = (( seq_id (vseq . m)) . 0 ) and

               A55: rseq0 is convergent and

               A56: (tseq . 0 ) = ( lim rseq0) by A38;



               A57: for m be Nat holds (rseq . m) = ( |.((rseq0 . m) - (( seq_id (vseq . n)) . 0 )).| to_power p)

              proof

                let m be Nat;

                (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 ) by A53

                .= ((( seq_id ((vseq . m) - (vseq . n))) rto_power p) . 0 ) by SERIES_1:def 1

                .= (((( seq_id (vseq . m)) - ( seq_id (vseq . n))) rto_power p) . 0 ) by A42

                .= ( |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 ).| to_power p) by Def1

                .= ( |.((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| to_power p) by SEQ_1: 7

                .= ( |.((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).| to_power p) by SEQ_1: 10

                .= ( |.((( seq_id (vseq . m)) . 0 ) - (( seq_id (vseq . n)) . 0 )).| to_power p);

                hence thesis by A54;

              end;



              then ( lim rseq) = ( |.(( lim rseq0) - (( seq_id (vseq . n)) . 0 )).| to_power p) by A1, A55, Lm8

              .= ( |.((tseq . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).| to_power p) by A56

              .= ( |.((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| to_power p) by SEQ_1: 10

              .= ( |.((tseq - ( seq_id (vseq . n))) . 0 ).| to_power p) by SEQ_1: 7

              .= (((( seq_id tseq) + ( - ( seq_id (vseq . n)))) rto_power p) . 0 ) by Def1

              .= (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . 0 ) by SERIES_1:def 1;

              hence thesis by A1, A55, A57, Lm8;

            end;

          end;

          then

           A58: P[ 0 ];

          for i be Nat holds P[i] from NAT_1:sch 2( A58, A52);

          hence thesis;

        end;

        let e2 be Real such that

         A59: e2 > 0 ;

        set e = (e2 / 2);

        reconsider e1 = (e to_power (1 / p)) as Real;

        e > 0 by A59, XREAL_1: 215;

        then e1 > 0 by POWER: 34;

        then

        consider k be Nat such that

         A60: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e1 by A4, RSSPACE3: 8;



         A61: for m,n be Nat st n >= k & m >= k holds ((( seq_id ((vseq . m) - (vseq . n))) rto_power p) is summable & ( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) < e & for i be Nat holds 0 <= ((( seq_id ((vseq . m) - (vseq . n))) rto_power p) . i))

        proof

          let m,n be Nat such that

           A62: n >= k and

           A63: m >= k;

           ||.((vseq . m) - (vseq . n)).|| < e1 by A60, A62, A63;

          then (the normF of lp . ((vseq . m) - (vseq . n))) < e1;

          then

           A64: (( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p)) < e1 by A3, Def3;



           A65: for i be Nat holds ((( seq_id ((vseq . m) - (vseq . n))) rto_power p) . i) >= 0

          proof

            let i be Nat;

            ((( seq_id ((vseq . m) - (vseq . n))) rto_power p) . i) = ( |.(( seq_id ((vseq . m) - (vseq . n))) . i).| to_power p) by Def1;

            hence thesis by A1, Lm1, COMPLEX1: 46;

          end;



           A66: (( seq_id ((vseq . m) - (vseq . n))) rto_power p) is summable by A1, A3, Th10;

          then

           A67: (( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p)) >= 0 by A2, A65, Lm1, SERIES_1: 18;



           A68: (e1 to_power p) = (e to_power ((1 / p) * p)) by A59, POWER: 33, XREAL_1: 215

          .= (e to_power 1) by A1, XCMPLX_1: 106

          .= e by POWER: 25;

          ((( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p)) to_power p) = (( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power ((1 / p) * p)) by A1, A2, A65, A66, HOLDER_1: 2, SERIES_1: 18

          .= ( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) by A5, POWER: 25;

          hence thesis by A1, A3, A65, A64, A68, A67, Th1, Th10;

        end;



         A69: e2 > e by A59, XREAL_1: 216;

        for n be Nat st n >= k holds ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) < e2

        proof

          let n be Nat such that

           A70: n >= k;



           A71: for i be Nat st 0 <= i holds (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i) <= e

          proof

            let i be Nat such that 0 <= i;

            deffunc F( Nat) = (( Partial_Sums (( seq_id ((vseq . $1) - (vseq . n))) rto_power p)) . i);

            consider rseq be Real_Sequence such that

             A72: for m be Nat holds (rseq . m) = F(m) from SEQ_1:sch 1;



             A73: for m be Nat st m >= k holds (rseq . m) <= e

            proof

              let m be Nat;



               A74: (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i) by A72;

              assume

               A75: m >= k;

              then

               A76: for i be Nat holds 0 <= ((( seq_id ((vseq . m) - (vseq . n))) rto_power p) . i) by A61, A70;

              (( seq_id ((vseq . m) - (vseq . n))) rto_power p) is summable by A61, A70, A75;

              then

               A77: (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i) <= ( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) by A76, RSSPACE2: 3;

              ( Sum (( seq_id ((vseq . m) - (vseq . n))) rto_power p)) < e by A61, A70, A75;

              hence thesis by A77, A74, XXREAL_0: 2;

            end;



             A78: ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i) by A41, A72;

            rseq is convergent by A41, A72;

            hence thesis by A78, A73, RSSPACE2: 5;

          end;

          now

            take e2 = (e + 1);



             A79: e2 > e by XREAL_1: 29;

            let i be Nat;

            (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i) <= e by A71, NAT_1: 2;

            hence (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) . i) < e2 by A79, XXREAL_0: 2;

          end;

          then

           A80: ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) is bounded_above by SEQ_2:def 3;



           A81: ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) = ( lim ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p))) by SERIES_1:def 3;



           A82: for i be Nat holds 0 <= (((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) . i)

          proof

            let i be Nat;

            (((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) . i) = ( |.((( seq_id tseq) - ( seq_id (vseq . n))) . i).| to_power p) by Def1;

            hence thesis by A1, Lm1, COMPLEX1: 46;

          end;

          then ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) is summable by A80, SERIES_1: 17;

          then ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) is convergent by SERIES_1:def 2;

          then ( lim ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p))) <= e by A71, RSSPACE2: 5;

          hence thesis by A69, A82, A80, A81, SERIES_1: 17, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      (( seq_id tseq) rto_power p) is summable

      proof

        consider m be Nat such that

         A83: for n be Nat st n >= m holds ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) < 1 by A40;



         A84: ((( seq_id tseq) - ( seq_id (vseq . m))) rto_power p) is summable by A83;

        set d = ( seq_id tseq);

        set b = ( seq_id (vseq . m));

        set a = (( seq_id tseq) - ( seq_id (vseq . m)));



         A85: (a + b) = ((( seq_id tseq) + ( seq_id (vseq . m))) + ( - ( seq_id (vseq . m)))) by SEQ_1: 13

        .= ((( seq_id tseq) + ( seq_id (vseq . m))) - ( seq_id (vseq . m)))

        .= d by Lm10;

        (( seq_id (vseq . m)) rto_power p) is summable by A1, A3, Def2;

        hence thesis by A1, A84, A85, Lm11;

      end;

      then

      reconsider tv = tseq as Point of lp by A1, A3, Th10;

      for e be Real st e > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((vseq . n) - tv).|| < e

      proof

        let e be Real such that

         A86: e > 0 ;

        set e1 = (e to_power p);

        consider m be Nat such that

         A87: for n be Nat st n >= m holds ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) < e1 by A40, A86, POWER: 34;

        now

          let n be Nat such that

           A88: n >= m;



           A89: ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) < e1 by A87, A88;

          for i be Nat holds (((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) . i) >= 0

          proof

            let i be Nat;

            (((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p) . i) = ( |.((( seq_id tseq) - ( seq_id (vseq . n))) . i).| to_power p) by Def1;

            hence thesis by A1, Lm1, COMPLEX1: 46;

          end;

          then

           A90: ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) rto_power p)) >= 0 by A87, A88, SERIES_1: 18;



           A91: (e1 to_power (1 / p)) = (e to_power (p * (1 / p))) by A86, POWER: 33

          .= (e to_power 1) by A1, XCMPLX_1: 106

          .= e by POWER: 25;

          (( Sum ((( seq_id tv) - ( seq_id (vseq . n))) rto_power p)) to_power (1 / p)) = (( Sum (( seq_id (( seq_id tv) - ( seq_id (vseq . n)))) rto_power p)) to_power (1 / p))

          .= (( Sum (( seq_id (tv - (vseq . n))) rto_power p)) to_power (1 / p)) by A1, A3, Th10

          .= ||.(tv + ( - (vseq . n))).|| by A3, Def3

          .= ||.( - ((vseq . n) - tv)).|| by RLVECT_1: 33

          .= ||.((vseq . n) - tv).|| by NORMSP_1: 2;

          hence ||.((vseq . n) - tv).|| < e by A2, A90, A89, A91, Th1;

        end;

        hence thesis;

      end;

      hence thesis by NORMSP_1:def 6;

    end;

    definition

      let p be Real;

      :: LP_SPACE:def4

      func l_Space^ p -> RealBanachSpace equals NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

      coherence

      proof

        set lp = NORMSTR (# ( the_set_of_RealSequences_l^ p), ( Zero_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Add_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( Mult_ (( the_set_of_RealSequences_l^ p), Linear_Space_of_RealSequences )), ( l_norm^ p) #);

        reconsider lp as RealNormSpace by A1, Th9, Th14;

        for vseq be sequence of lp st vseq is Cauchy_sequence_by_Norm holds vseq is convergent by A1, Th16;

        hence thesis by LOPBAN_1:def 15;

      end;

    end