:: The Banach Space $l^p$
::  by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SEQ_1, REAL_1, SUBSET_1, FUNCT_1, COMPLEX1, POWER,
      XXREAL_0, XBOOLE_0, RSSPACE, SERIES_1, CARD_1, TARSKI, RELAT_1, ARYTM_3,
      CARD_3, RLVECT_1, RSSPACE3, NORMSP_1, RLSUB_1, XXREAL_2, VALUED_0,
      VALUED_1, ALGSTR_0, ZFMISC_1, STRUCT_0, SUPINF_2, REALSET1, ARYTM_1,
      SEQ_2, ORDINAL2, PRE_TOPC, NAT_1, LOPBAN_1, LP_SPACE, NORMSP_0, METRIC_1,
      RELAT_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1,
      REALSET1, PARTFUN1, FUNCT_2, PRE_TOPC, DOMAIN_1, XXREAL_0, XREAL_0,
      XCMPLX_0, ORDINAL1, NUMBERS, RLVECT_1, COMPLEX1, REAL_1, NAT_1, STRUCT_0,
      ALGSTR_0, RLSUB_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1,
      POWER, RSSPACE, RSSPACE3, LOPBAN_1;
 constructors REAL_1, COMPLEX1, SEQ_2, PREPOWER, SERIES_1, REALSET1, RLSUB_1,
      RSSPACE3, LOPBAN_1, RELSET_1, BINOP_2, COMSEQ_2, BINOP_1, FUNCSDOM,
      SEQ_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
      XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, LOPBAN_1, VALUED_0,
      RSSPACE, VALUED_1, FUNCT_2, SERIES_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, NORMSP_0;
 equalities REALSET1, BINOP_1, RLVECT_1, STRUCT_0, ALGSTR_0, VALUED_1,
      NORMSP_0, RSSPACE, SEQ_1, FUNCSDOM;
 expansions NORMSP_0;
 theorems XBOOLE_0, RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQM_3,
      SERIES_1, COMSEQ_3, FUNCT_1, NAT_1, SEQ_2, FUNCT_2, RLVECT_1, RLSUB_1,
      NORMSP_1, XREAL_0, RSSPACE2, XCMPLX_1, SEQ_4, POWER, RSSPACE, RSSPACE3,
      LOPBAN_1, HOLDER_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
 schemes NAT_1, SEQ_1, FUNCT_2, XBOOLE_0;

begin :: The Real Norm Space of l^p Real Sequences

definition
  let x be Real_Sequence;
  let p be Real;
  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;
  func the_set_of_RealSequences_l^p -> non empty Subset of
  Linear_Space_of_RealSequences means
  :Def2:
  for x being 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 being set such that
A2: for x being 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 being set holds x in X1 iff x in the_set_of_RealSequences &
    seq_id(x) rto_power p is summable and
A5: for x being 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,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 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,37;
end;

Lm3: for p be Real st 1 = p for a,b be Real_Sequence 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 Th2:
  for p be Real st 1 <= p for a,b be Real_Sequence
   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 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,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,def 3;
A19: ||.a1+b1.|| =Sum(abs(seq_id(a1+b1))) by RSSPACE3:def 2,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 Th3:
  for a,b be Real_Sequence 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 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,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,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;
        thus
A32:    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,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
  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,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 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
  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
  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;
  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 being Function of the_set_of_RealSequences_l^p,REAL st for x being
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 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 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 :: The Banach Space of l^p Real Sequences

theorem 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 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 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,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,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 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 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 Th12:
  for p be Real st 1 <=p 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 being 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 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 #)
for x being 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 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 #)
 for x being 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 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 #)
 for x being 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 Th13:
  for p be Real st 1 <= p 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 #)
 for x, y being 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,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 Th14:
  for p be Real st p >= 1 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 being 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
  for p be Real st p >= 1 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
for c be Real, seq be Real_Sequence st seq is
convergent 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
 for c be Real, seq, seq1 be Real_Sequence st seq
is convergent & seq1 is convergent 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
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 Th16:
  for p be Real st 1 <=p 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 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 being 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
  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 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 being 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 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 such that
A1: 1 <= p;
  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;