:: Real Linear Space of Real Sequences
::  by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-2012 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, XBOOLE_0, SEQ_1, FUNCT_2, TARSKI, REAL_1, BINOP_1,
      SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, CARD_1, FUNCOP_1, NAT_1,
      RLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, XREAL_0,
      ORDINAL1, RLSUB_1, REALSET1, SERIES_1, XXREAL_0, SQUARE_1, CARD_3,
      BHSP_1, COMPLEX1, SEQ_2, ORDINAL2, XXREAL_2, VALUED_0, RSSPACE;
 notations TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, NAT_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, REALSET1, FUNCOP_1, RLVECT_1, RLSUB_1,
      BHSP_1, SQUARE_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, BINOP_1;
 constructors PARTFUN1, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D,
      SEQ_2, SEQM_3, SERIES_1, REALSET1, RLSUB_1, BHSP_1, SEQ_1, VALUED_1,
      RELSET_1, COMSEQ_2;
 registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
      REALSET1, STRUCT_0, RLVECT_1, BHSP_1, ALGSTR_0, VALUED_1, FUNCT_2,
      VALUED_0, SERIES_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions SQUARE_1, BINOP_1, TARSKI, RLVECT_1, XBOOLE_0, REALSET1, STRUCT_0,
      ALGSTR_0;
 theorems XBOOLE_0, RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3,
      SERIES_1, COMSEQ_3, INT_1, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, RLSUB_1,
      SEQ_4, BINOP_1, FUNCOP_1, XREAL_1, ORDINAL1, ALGSTR_0, XREAL_0;
 schemes NAT_1, BINOP_1, XBOOLE_0, BINOP_2;

begin

definition
  func the_set_of_RealSequences -> non empty set means
  :Def1:
  for x being set holds x in it iff x is Real_Sequence;
  existence
  proof
    defpred P[set] means $1 is Real_Sequence;
    consider IT being set such that
A1: for x being set holds x in IT iff x in Funcs(NAT,REAL) & P[x] from
    XBOOLE_0:sch 1;
    IT is non empty
    proof
      set zeroseq = the Real_Sequence;
      zeroseq in Funcs(NAT,REAL) by FUNCT_2:8;
      hence thesis by A1;
    end;
    then reconsider IT as non empty set;
    take IT;
    for x being set holds x is Real_Sequence implies x in IT
    proof
      let x be set;
      assume
A2:   x is Real_Sequence;
      then x in Funcs(NAT,REAL) by FUNCT_2:8;
      hence thesis by A1,A2;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let X1,X2 be non empty set;
    assume that
A3: for x being set holds x in X1 iff x is Real_Sequence and
A4: for x being set holds x in X2 iff x is Real_Sequence;
A5: X2 c= X1
    proof
      let x be set;
      assume x in X2;
      then x is Real_Sequence by A4;
      hence thesis by A3;
    end;
    X1 c= X2
    proof
      let x be set;
      assume x in X1;
      then x is Real_Sequence by A3;
      hence thesis by A4;
    end;
    hence thesis by A5,XBOOLE_0:def 10;
  end;
end;

definition
  let a be set such that
A1: a in the_set_of_RealSequences;
  func seq_id(a) -> Real_Sequence equals
  :Def2:
  a;
  coherence by A1,Def1;
end;

definition
  let a be set such that
A1: a in REAL;
  func R_id(a) -> Real equals
  :Def3:
  a;
  coherence by A1;
end;

definition
  func l_add -> BinOp of the_set_of_RealSequences means
  :Def4:
  for a,b being
  Element of the_set_of_RealSequences holds it.(a,b) = seq_id(a)+seq_id(b);
  existence
proof
  defpred P[Element of the_set_of_RealSequences, Element of
the_set_of_RealSequences,Element of the_set_of_RealSequences] means $3=seq_id(
  $1)+seq_id($2);
A1: for x,y being Element of the_set_of_RealSequences ex z being Element of
  the_set_of_RealSequences st P[x,y,z]
  proof
    let x,y be Element of the_set_of_RealSequences;
    seq_id(x)+seq_id(y) is Element of the_set_of_RealSequences by Def1;
    hence thesis;
  end;
  ex ADD be BinOp of the_set_of_RealSequences st for a,b being Element of
  the_set_of_RealSequences holds P[a,b,ADD.(a,b)] from BINOP_1:sch 3(A1);
  then consider ADD be BinOp of the_set_of_RealSequences such that
A2: for a,b being Element of the_set_of_RealSequences holds ADD.(a,b) =
  seq_id(a)+seq_id(b);
  thus thesis by A2;
end;
  uniqueness
  proof
    deffunc O(Element of the_set_of_RealSequences, Element of
    the_set_of_RealSequences)=seq_id($1)+seq_id($2);
    for o1,o2 being BinOp of the_set_of_RealSequences st (for a,b being
Element of the_set_of_RealSequences holds o1.(a,b) = O(a,b)) & (for a,b being
Element of the_set_of_RealSequences holds o2.(a,b) = O(a,b)) holds o1 = o2 from
    BINOP_2:sch 2;
    hence thesis;
  end;
end;

definition
  func l_mult -> Function of [: REAL, the_set_of_RealSequences :],
  the_set_of_RealSequences means
  :Def5:
  for r,x be set st r in REAL & x in
  the_set_of_RealSequences holds it.(r,x) = R_id(r)(#)seq_id(x);
  existence
proof
  deffunc F(set,set) = R_id($1) (#) seq_id($2);
A1: for r,x be set st r in REAL & x in the_set_of_RealSequences holds F(r,x)
  in the_set_of_RealSequences by Def1;
  ex f be Function of [:REAL, the_set_of_RealSequences:],
  the_set_of_RealSequences st for r,x be set st r in REAL & x in
  the_set_of_RealSequences holds f.(r,x) = F(r,x) from BINOP_1:sch 2(A1);
  hence thesis;
end;
  uniqueness
  proof
    let mult1,mult2 be Function of [: REAL, the_set_of_RealSequences :],
    the_set_of_RealSequences such that
A2: for r,x be set st r in REAL & x in the_set_of_RealSequences holds
    mult1.(r,x) = R_id(r)(#)seq_id(x) and
A3: for r,x be set st r in REAL & x in the_set_of_RealSequences holds
    mult2.(r,x) = R_id(r)(#)seq_id(x);
    for r being Element of REAL for x being Element of
    the_set_of_RealSequences holds mult1.(r,x) = mult2.(r,x)
    proof
      let r being Element of REAL;
      let x being Element of the_set_of_RealSequences;
      thus mult1.(r,x) = R_id(r)(#)seq_id(x) by A2
        .= mult2.(r,x) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  func Zeroseq -> Element of the_set_of_RealSequences means
  :Def6:
  for n be Element of NAT holds (seq_id it).n=0;
  existence
  proof
    reconsider zeroseq = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
    zeroseq in the_set_of_RealSequences by Def1;
    then
A1: seq_id zeroseq = zeroseq by Def2;
    reconsider zeroseq as Element of the_set_of_RealSequences by Def1;
    take zeroseq;
    let n be Nat;
    thus thesis by A1,FUNCOP_1:7;
  end;
  uniqueness
  proof
    let x,y be Element of the_set_of_RealSequences such that
A2: for n be Element of NAT holds (seq_id x).n=0 and
A3: for n be Element of NAT holds (seq_id y).n=0;
A4: for s be set st s in NAT holds (seq_id x).s = (seq_id y).s
    proof
      let s be set;
      assume
A5:   s in NAT;
      then (seq_id y).s = 0 by A3;
      hence thesis by A2,A5;
    end;
    x=seq_id x by Def2
      .=seq_id y by A4,FUNCT_2:12;
    hence thesis by Def2;
  end;
end;

theorem Th1:
  for x be Real_Sequence holds seq_id x = x
proof
  let x be Real_Sequence;
  reconsider x1=x as set;
  x1 in the_set_of_RealSequences by Def1;
  hence thesis by Def2;
end;

theorem
  for v,w being VECTOR of RLSStruct(#the_set_of_RealSequences,Zeroseq,
    l_add,l_mult#) holds v + w = seq_id(v)+seq_id(w) by Def4;

theorem Th3:
  for r being Real, v being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds r * v = r(#)seq_id(v)
proof
  let r be Real;
  let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq, l_add,
    l_mult #);
  thus r*v = R_id(r)(#)seq_id(v) by Def5
    .= r(#)seq_id(v) by Def3;
end;

registration
  cluster RLSStruct (# the_set_of_RealSequences, Zeroseq, l_add, l_mult #) ->
    Abelian;
  coherence
  proof
    let v,w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add
      ,l_mult #);
    v + w = seq_id(v)+seq_id(w) by Def4;
    hence thesis by Def4;
  end;
end;

theorem Th4:
  for u,v,w being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) holds (u + v) + w = u + (v + w)
proof
  let u,v,w be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,
    l_mult #);
  (u+v) + w = seq_id(u+v)+seq_id(w) by Def4
    .= seq_id(seq_id(u)+seq_id(v))+seq_id(w) by Def4
    .= (seq_id(u)+seq_id(v)) +seq_id(w) by Th1
    .= seq_id(u)+(seq_id(v)+seq_id(w)) by SEQ_1:13
    .= seq_id(u)+seq_id(seq_id(v)+seq_id(w)) by Th1
    .= seq_id(u) + seq_id(v+w) by Def4;
  hence thesis by Def4;
end;

theorem Th5:
  for v being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) holds v + 0.RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) = v
proof
  set V=RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
  let v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,
    l_mult #);
A1: for s be set st s in NAT holds (seq_id(v)+seq_id(Zeroseq)).s=(seq_id v). s
  proof
    let s be set such that
A2: s in NAT;
    (seq_id(v)+seq_id(Zeroseq)).s = (seq_id v).s+(seq_id Zeroseq).s by A2,
SEQ_1:7
      .= (seq_id v).s + 0 by A2,Def6;
    hence thesis;
  end;
  v + 0.V = seq_id(v)+seq_id(Zeroseq) by Def4;
  hence v + 0.V=seq_id(v) by A1,FUNCT_2:12
    .=v by Def2;
end;

theorem Th6:
  for v being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) ex w being VECTOR of RLSStruct(#
    the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0.RLSStruct(#
    the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
proof
  set V = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
  let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult
  #);
  reconsider w=-seq_id(v) as VECTOR of V by Def1;
  for s be set st s in NAT holds (seq_id(v)+(-seq_id(v)) ).s=(seq_id(
  Zeroseq)).s
  proof
    let s be set such that
A1: s in NAT;
    (seq_id(v)+(-seq_id(v))).s = (seq_id(v)).s+(-seq_id(v)).s by A1,SEQ_1:7
      .= (seq_id(v)).s + (-((seq_id(v)).s)) by A1,SEQ_1:10
      .= (seq_id(Zeroseq)).s by A1,Def6;
    hence thesis;
  end;
  then
A2: seq_id(v)+(-seq_id(v)) = seq_id(Zeroseq) by FUNCT_2:12
    .=Zeroseq by Def2;
  v+w = seq_id(v)+seq_id(w) by Def4
    .= seq_id(v)+(-seq_id(v)) by Th1;
  hence thesis by A2;
end;

theorem Th7:
  for a being Real, v,w being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds a * (v + w) = a * v + a
  * w
proof
  let a be Real;
  let v,w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,
    l_mult #);
A1: a * (v + w) =a(#)seq_id(v + w) by Th3
    .=a(#)seq_id(seq_id(v) + seq_id(w)) by Def4
    .=a(#)(seq_id(v) + seq_id(w)) by Th1
    .=a(#)seq_id(v) + a(#)seq_id(w) by SEQ_1:22;
  a*v + a*w = seq_id(a*v)+seq_id(a*w) by Def4
    .=seq_id(a(#)seq_id(v)) + seq_id(a*w) by Th3
    .=seq_id(a(#)seq_id(v)) + seq_id(a(#)seq_id(w)) by Th3
    .=a(#)seq_id(v) + seq_id(a(#)seq_id(w)) by Th1
    .=a(#)seq_id(v) + a(#)seq_id(w) by Th1;
  hence thesis by A1;
end;

theorem Th8:
  for a,b being Real, v being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a + b) * v = a * v + b
  * v
proof
  let a,b be Real;
  let v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,
    l_mult #);
  for s be set st s in NAT holds ((a+b)(#)seq_id(v)).s=(a(#)seq_id(v)+b(#)
  seq_id(v)).s
  proof
    let s be set such that
A1: s in NAT;
    ((a+b)(#)seq_id(v)).s = (a+b)*(seq_id(v)).s by A1,SEQ_1:9
      .= a*((seq_id(v)).s)+b*((seq_id(v)).s)
      .= (a(#)seq_id(v)).s+b*(seq_id(v)).s by A1,SEQ_1:9
      .= (a(#)seq_id(v)).s+(b(#)seq_id(v)).s by A1,SEQ_1:9;
    hence thesis by A1,SEQ_1:7;
  end;
  then
A2: (a+b)(#)seq_id(v) =a(#)seq_id(v)+b(#)seq_id(v) by FUNCT_2:12;
  a*v + b*v = seq_id(a*v)+seq_id(b*v) by Def4
    .=seq_id(a(#)seq_id(v)) + seq_id(b*v) by Th3
    .=seq_id(a(#)seq_id(v)) + seq_id(b(#)seq_id(v)) by Th3
    .=a(#)seq_id(v) + seq_id(b(#)seq_id(v)) by Th1
    .=a(#)seq_id(v) + b(#)seq_id(v) by Th1;
  hence thesis by A2,Th3;
end;

theorem Th9:
  for a,b be Real, v being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a * b) * v = a * (b * v
  )
proof
  let a,b be Real;
  let v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,
    l_mult #);
  (a * b) * v =(a*b)(#)seq_id(v) by Th3
    .=a(#)(b(#)seq_id(v)) by SEQ_1:23
    .=a(#)seq_id(b(#)seq_id(v)) by Th1
    .=a(#)seq_id(b*v) by Th3;
  hence thesis by Th3;
end;

theorem Th10:
  for v being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) holds 1 * v = v
proof
  let v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,
    l_mult #);
  1 * v =1(#)seq_id(v) by Th3
    .=seq_id(v) by SEQ_1:27;
  hence thesis by Def2;
end;

definition
  func Linear_Space_of_RealSequences -> RLSStruct equals
  RLSStruct (#
    the_set_of_RealSequences, Zeroseq, l_add, l_mult #);
  correctness;
end;

registration
  cluster Linear_Space_of_RealSequences -> strict non empty;
  coherence;
end;

registration
  cluster Linear_Space_of_RealSequences -> Abelian add-associative
    right_zeroed right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital;
  coherence
  proof
    set S = Linear_Space_of_RealSequences;
    thus S is Abelian;
    thus S is add-associative
    proof
      let u,v,w be Element of S;
      thus thesis by Th4;
    end;
    thus S is right_zeroed
    proof
      let v be Element of S;
      thus thesis by Th5;
    end;
    thus S is right_complementable
    proof
      let v be Element of S;
      thus ex w being VECTOR of S st v + w = 0.S by Th6;
    end;
    thus for a being real number for v,w being VECTOR of S holds a * (v + w) =
    a * v + a * w
    proof
      let a be real number;
      reconsider a as Real by XREAL_0:def 1;
      for v,w being VECTOR of S holds a * (v + w) = a * v + a * w by Th7;
      hence thesis;
    end;
    thus for a,b being real number for v being VECTOR of S holds (a + b) * v =
    a * v + b * v
    proof
      let a,b be real number;
      reconsider a,b as Real by XREAL_0:def 1;
      for v being VECTOR of S holds (a + b) * v = a * v + b * v by Th8;
      hence thesis;
    end;
    thus for a,b being real number for v being VECTOR of S holds (a * b) * v =
    a * (b * v)
    proof
      let a,b be real number;
      reconsider a,b as Real by XREAL_0:def 1;
      for v being VECTOR of S holds (a * b) * v = a * (b * v) by Th9;
      hence thesis;
    end;
    let v be VECTOR of S;
    thus thesis by Th10;
  end;
end;

definition
  let X be RealLinearSpace;
  let X1 be Subset of X such that
B1: X1 is linearly-closed non empty;
  func Add_(X1,X) -> BinOp of X1 equals
  :Def8:
  (the addF of X)||X1;
  correctness
  proof
A1: dom (the addF of X) = [:the carrier of X,the carrier of X:] by
FUNCT_2:def 1;
A2: for z be set st z in [:X1,X1:] holds ((the addF of X)||X1).z in X1
    proof
      let z be set such that
A3:   z in [:X1,X1:];
      consider r,x be set such that
A4:   r in X1 & x in X1 and
A5:   z=[r,x] by A3,ZFMISC_1:def 2;
      reconsider y=x,r1=r as VECTOR of X by A4;
      [r,x] in dom ((the addF of X)||X1) by A1,A3,A5,RELAT_1:62,ZFMISC_1:96;
      then ((the addF of X)||X1).z = r1+y by A5,FUNCT_1:47;
      hence thesis by B1,A4,RLSUB_1:def 1;
    end;
    dom ((the addF of X)||X1) =[:X1,X1:] by A1,RELAT_1:62,ZFMISC_1:96;
    hence thesis by A2,FUNCT_2:3;
  end;
end;

definition
  let X be RealLinearSpace;
  let X1 be Subset of X such that
B1: X1 is linearly-closed non empty;
  func Mult_(X1,X) -> Function of [:REAL,X1:], X1 equals
  :Def9:
  (the Mult of X) | [:REAL,X1:];
  correctness
  proof
A1: [:REAL,X1:] c= [:REAL,the carrier of X:] & dom (the Mult of X) = [:
    REAL,the carrier of X:] by FUNCT_2:def 1,ZFMISC_1:95;
A2: for z be set st z in [:REAL,X1:] holds ((the Mult of X) | [:REAL,X1:])
    .z in X1
    proof
      let z be set such that
A3:   z in [:REAL,X1:];
      consider r,x be set such that
A4:   r in REAL and
A5:   x in X1 and
A6:   z=[r,x] by A3,ZFMISC_1:def 2;
      reconsider r as Real by A4;
      reconsider y=x as VECTOR of X by A5;
      [r,x] in dom ((the Mult of X) | [:REAL,X1:]) by A1,A3,A6,RELAT_1:62;
      then ((the Mult of X) | [:REAL,X1:]).z = r*y by A6,FUNCT_1:47;
      hence thesis by B1,A5,RLSUB_1:def 1;
    end;
    dom ((the Mult of X) | [:REAL,X1:]) =[:REAL,X1:] by A1,RELAT_1:62;
    hence thesis by A2,FUNCT_2:3;
  end;
end;

definition
  let X be RealLinearSpace, X1 be Subset of X such that
A1: X1 is linearly-closed non empty;
  func Zero_(X1,X) -> Element of X1 equals
  :Def10:
  0.X;
  correctness
  proof
    set v = the Element of X1;
    v in X1 by A1;
    then reconsider v as Element of X;
    v-v=0.X by RLVECT_1:15;
    hence thesis by A1,RLSUB_1:3;
  end;
end;

theorem Th11:
  for V be RealLinearSpace, V1 be Subset of V st V1 is
linearly-closed non empty holds RLSStruct (# V1,Zero_(V1,V), Add_(V1,V),Mult_(
    V1,V) #) is Subspace of V
proof
  let V be RealLinearSpace;
  let V1 be Subset of V such that
A1: V1 is linearly-closed non empty;
A2: Mult_(V1,V) = (the Mult of V) | [:REAL,V1:] by A1,Def9;
  Zero_(V1,V) = 0.V & Add_(V1,V)= (the addF of V)||V1 by A1,Def8,Def10;
  hence thesis by A1,A2,RLSUB_1:24;
end;

definition
  func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences
  means
  :Def11:
  for x being set holds x in it iff x in the_set_of_RealSequences &
  seq_id(x)(#)seq_id(x) is summable;
  existence
  proof
    defpred P[set] means seq_id($1)(#)seq_id($1) is summable;
    consider IT being set such that
A1: for x being set holds x in IT iff x in the_set_of_RealSequences &
    P[x] from XBOOLE_0:sch 1;
    for x be set st x in IT holds x in the_set_of_RealSequences by A1;
    then IT is Subset of the_set_of_RealSequences by TARSKI:def 3;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let X1,X2 be Subset of Linear_Space_of_RealSequences;
    assume that
A2: for x being set holds x in X1 iff x in the_set_of_RealSequences &
    seq_id(x)(#)seq_id(x) is summable and
A3: for x being set holds x in X2 iff x in the_set_of_RealSequences &
    seq_id(x)(#)seq_id(x) is summable;
    thus X1 c= X2
    proof
      let x be set;
      assume
A4:   x in X1;
      then seq_id(x)(#)seq_id(x) is summable by A2;
      hence thesis by A3,A4;
    end;
    let x be set;
    assume
A5: x in X2;
    then seq_id(x)(#)seq_id(x) is summable by A3;
    hence thesis by A2,A5;
  end;
end;

registration
  cluster the_set_of_l2RealSequences -> linearly-closed non empty;
  coherence
  proof
    set W = the_set_of_l2RealSequences;
A1: 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;
      assume v in W;
      then
A2:   (seq_id(v))(#)(seq_id(v)) is summable by Def11;
      seq_id(a*v)=seq_id(a(#)seq_id(v)) by Th3
        .=a(#)seq_id(v) by Th1;
      then (seq_id(a*v))(#)(seq_id(a*v)) =a(#)((a(#)seq_id(v))(#) seq_id(v))
      by SEQ_1:19
        .=a(#)(a(#)( seq_id(v)(#)seq_id(v))) by SEQ_1:18
        .=(a*a)(#)(seq_id(v)(#)seq_id(v)) by SEQ_1:23;
      then (seq_id(a*v))(#)(seq_id(a*v)) is summable by A2,SERIES_1:10;
      hence thesis by Def11;
    end;
A3: for v,u be VECTOR of Linear_Space_of_RealSequences st v in
    the_set_of_l2RealSequences & u in the_set_of_l2RealSequences holds v + u in
    the_set_of_l2RealSequences
    proof
      let v,u be VECTOR of Linear_Space_of_RealSequences such that
A4:   v in W and
A5:   u in W;
      (seq_id(v+u))(#)(seq_id(v+u)) is summable
      proof
        set r = (seq_id(v+u))(#)(seq_id(v+u));
        set q = (seq_id(u))(#)(seq_id(u));
        set p = (seq_id(v))(#)(seq_id(v));
A6:     for n be Element of NAT holds 0<=r.n
        proof
          let n be Element of NAT;
          r.n=(seq_id(v+u)).n * (seq_id(v+u)).n by SEQ_1:8;
          hence thesis by XREAL_1:63;
        end;
A7:     for n be Element of NAT holds r.n <=(2(#)p+2(#)q).n
        proof
          set s = seq_id v, t = seq_id u;
          let n be Element of NAT;
          reconsider sn=s.n, tn=t.n as Real;
A8:       (2(#)p+2(#)q).n=(2(#)p).n +(2(#)q).n by SEQ_1:7
            .= 2*p.n + (2(#)q).n by SEQ_1:9
            .= 2*p.n + 2*q.n by SEQ_1:9
            .= 2*(s.n*s.n) + 2*q.n by SEQ_1:8
            .= 2*sn^2 + 2*tn^2 by SEQ_1:8;
A9:       0 <= (sn-tn)^2 by XREAL_1:63;
A10:      seq_id(v+u)=seq_id(seq_id(v)+seq_id(u)) by Def4
            .=seq_id(v)+seq_id(u) by Th1;
          r.n=(seq_id(v+u)).n * (seq_id(v+u)).n by SEQ_1:8
            .=(s.n+t.n) * (seq_id(v)+seq_id(u)).n by A10,SEQ_1:7
            .=((s.n)+(t.n))^2 by SEQ_1:7
            .= sn^2 + 2*sn*tn + tn^2;
          then 0 + r.n <= (2(#)p+2(#)q).n - r.n + r.n by A8,A9,XREAL_1:7;
          hence thesis;
        end;
        (seq_id u)(#)(seq_id u) is summable by A5,Def11;
        then
A11:    2(#)q is summable by SERIES_1:10;
        (seq_id v)(#)(seq_id v) is summable by A4,Def11;
        then 2(#)p is summable by SERIES_1:10;
        then 2(#)p+2(#)q is summable by A11,SERIES_1:7;
        hence thesis by A6,A7,SERIES_1:20;
      end;
      hence thesis by Def11;
    end;
    seq_id Zeroseq (#)seq_id Zeroseq is absolutely_summable
    proof
      reconsider rseq=(seq_id(Zeroseq)(#)seq_id Zeroseq) as Real_Sequence;
      now
        let n be Element of NAT;
        thus rseq.n =((seq_id Zeroseq).n ) * ((seq_id Zeroseq).n) by SEQ_1:8
          .=((seq_id Zeroseq).n ) * 0 by Def6
          .=0;
      end;
      hence thesis by COMSEQ_3:3;
    end;
    hence thesis by A3,A1,Def11,RLSUB_1:def 1;
  end;
end;

theorem
  RLSStruct(# the_set_of_l2RealSequences, Zero_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #) is Subspace of
  Linear_Space_of_RealSequences by Th11;

theorem Th13:
  RLSStruct (# the_set_of_l2RealSequences, Zero_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #) is RealLinearSpace
  by Th11;

theorem
  the carrier of Linear_Space_of_RealSequences =
  the_set_of_RealSequences & (for x be set holds x is VECTOR of
  Linear_Space_of_RealSequences iff x is Real_Sequence ) & (for u be VECTOR of
  Linear_Space_of_RealSequences holds u =seq_id(u) ) & (for u,v be VECTOR of
Linear_Space_of_RealSequences holds u+v =seq_id(u)+seq_id(v) ) & for r be Real
  for u be VECTOR of Linear_Space_of_RealSequences holds r*u =r(#)seq_id(u) by
Def1,Def2,Def4,Th3;

definition
  func l_scalar -> Function of [:the_set_of_l2RealSequences,
  the_set_of_l2RealSequences:], REAL means
  for x,y be set st x in
  the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds it.(x,y) =
  Sum(seq_id(x)(#)seq_id(y));
  existence
proof
  deffunc F(set,set) = Sum(seq_id($1)(#)seq_id($2));
  set X = the_set_of_l2RealSequences;
A1: for x,y being set st x in X & y in X holds F(x,y) in REAL;
  ex f being Function of [:X,X:],REAL st for x,y being set st x in X & y
  in X holds f.(x,y) = F(x,y) from BINOP_1:sch 2(A1);
  hence thesis;
end;
  uniqueness
  proof
    set X = the_set_of_l2RealSequences;
    let scalar1, scalar2 be Function of [: X, X :], REAL such that
A2: for x,y be set st x in X & y in X holds scalar1.(x,y) = Sum(seq_id
    (x)(#)seq_id(y)) and
A3: for x,y be set st x in X & y in X holds scalar2.(x,y) = Sum(seq_id
    (x)(#)seq_id(y));
    for x, y be set st x in X & y in X holds scalar1.(x,y) = scalar2.(x,y)
    proof
      let x,y be set such that
A4:   x in X & y in X;
      thus scalar1.(x,y) = Sum(seq_id(x)(#)seq_id(y)) by A2,A4
        .= scalar2.(x,y) by A3,A4;
    end;
    hence thesis by BINOP_1:1;
  end;
end;

registration
  cluster UNITSTR (# the_set_of_l2RealSequences, Zero_(
      the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(
      the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_l2RealSequences,Linear_Space_of_RealSequences), l_scalar #) -> non
    empty;
  coherence;
end;

definition
  func l2_Space -> non empty UNITSTR equals
  UNITSTR (#
    the_set_of_l2RealSequences, Zero_(the_set_of_l2RealSequences,
    Linear_Space_of_RealSequences), Add_(the_set_of_l2RealSequences,
    Linear_Space_of_RealSequences), Mult_(the_set_of_l2RealSequences,
    Linear_Space_of_RealSequences), l_scalar #);
  coherence;
end;

theorem Th15:
  for l be RLSStruct st the RLSStruct of l is RealLinearSpace
  holds l is RealLinearSpace
proof
  let l be RLSStruct such that
A1: the RLSStruct of l is RealLinearSpace;
  reconsider l as non empty RLSStruct by A1;
  reconsider l0=RLSStruct (# the carrier of l, 0.l, the addF of l, the Mult of
    l #) as RealLinearSpace by A1;
A2: l is Abelian
  proof
    let v,w be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    reconsider w1=w as VECTOR of l0;
    thus v+w =v1+w1 .= w1+v1
      .= w +v;
  end;
A3: l is right_zeroed
  proof
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    thus v+0.l= v1 + 0.l0 .= v by RLVECT_1:def 4;
  end;
A4: l is right_complementable
  proof
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    consider w1 being VECTOR of l0 such that
A5: v1 + w1 = 0.l0 by ALGSTR_0:def 11;
    reconsider w = w1 as VECTOR of l;
    take w;
    thus thesis by A5;
  end;
A6: for v being VECTOR of l holds 1 * v = v
  proof
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    thus 1*v= 1*v1 .= v by RLVECT_1:def 8;
  end;
A7: for a,b be real number for v being VECTOR of l holds (a * b) * v = a *
  (b * v)
  proof
    let a,b be real number;
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    thus (a*b)*v =(a*b)*v1 .=a*(b*v1) by RLVECT_1:def 7
      .= a*(b*v);
  end;
A8: for a,b be real number for v being VECTOR of l holds (a + b) * v = a *
  v + b * v
  proof
    let a,b be real number;
    let v be VECTOR of l;
    reconsider v1=v as VECTOR of l0;
    thus (a+b)*v =(a+b)*v1 .=a*v1+b*v1 by RLVECT_1:def 6
      .= a*v +b*v;
  end;
A9: for a be real number for v,w being VECTOR of l holds a * (v + w) = a *
  v + a * w
  proof
    let a be real number;
    let v,w be VECTOR of l;
    reconsider v1=v, w1=w as VECTOR of l0;
    thus a*(v+w) =a*(v1+w1) .=a*v1+a*w1 by RLVECT_1:def 5
      .= a*v +a*w;
  end;
  l is add-associative
  proof
    let u,v,w be VECTOR of l;
    reconsider u1=u, v1=v, w1=w as VECTOR of l0;
    thus (u + v) + w = (u1+v1)+w1 .= u1+(v1+w1) by RLVECT_1:def 3
      .= u+(v+w);
  end;
  hence thesis by A2,A3,A4,A9,A8,A7,A6,RLVECT_1:def 5,def 6,def 7,def 8;
end;

theorem
  for rseq be Real_Sequence st (for n be Element of NAT holds rseq.n=0)
  holds rseq is summable & Sum rseq = 0
proof
  let rseq be Real_Sequence such that
A1: for n be Element of NAT holds rseq.n=0;
A2: for m be Element of NAT holds Partial_Sums (rseq).m = 0
  proof
    defpred P[Nat] means rseq.$1 = (Partial_Sums rseq).$1;
    let m be Element of NAT;
A3: for k be Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT such that
A4:   rseq.k = (Partial_Sums (rseq)).k;
      thus rseq.(k+1) = 0 + (rseq).(k+1) .= rseq.k + rseq.(k+1) by A1
        .= (Partial_Sums rseq).(k+1) by A4,SERIES_1:def 1;
    end;
A5: P[0] by SERIES_1:def 1;
    for n be Element of NAT holds P[n] from NAT_1:sch 1(A5,A3);
    hence (Partial_Sums rseq).m = rseq.m .= 0 by A1;
  end;
A6: for p be real number st 0<p ex n be Element of NAT st for m be Element
  of NAT st n<=m holds abs((Partial_Sums rseq).m-0)<p
  proof
    let p be real number such that
A7: 0<p;
    take 0;
    let m be Element of NAT such that
    0<=m;
    abs((Partial_Sums rseq).m-0) = abs(0-0) by A2
      .= 0 by ABSVALUE:def 1;
    hence thesis by A7;
  end;
  then
A8: Partial_Sums rseq is convergent by SEQ_2:def 6;
  then lim (Partial_Sums rseq) = 0 by A6,SEQ_2:def 7;
  hence thesis by A8,SERIES_1:def 2,def 3;
end;

theorem
  for rseq be Real_Sequence st (for n be Element of NAT holds 0 <= rseq.
n) & rseq is summable & Sum rseq=0 holds for n be Element of NAT holds rseq.n =
  0
proof
  let rseq be Real_Sequence such that
A1: for n be Element of NAT holds 0 <= rseq.n and
A2: rseq is summable and
A3: Sum rseq=0;
A4: Partial_Sums rseq is bounded_above by A1,A2,SERIES_1:17;
A5: for n be Nat holds (Partial_Sums rseq).n <= Sum rseq
  proof
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    then (Partial_Sums(rseq)).n <= lim Partial_Sums rseq by A1,A4,SEQ_4:37
,SERIES_1:16;
    hence thesis by SERIES_1:def 3;
  end;
A6: Partial_Sums rseq is non-decreasing by A1,SERIES_1:16;
  now
    given n1 be Element of NAT such that
A7: rseq.n1 <> 0;
A8: for n be Element of NAT holds 0 <= Partial_Sums(rseq).n
    proof
      let n be Element of NAT;
A9:   n=n+0 & Partial_Sums(rseq).0 = rseq.0 by SERIES_1:def 1;
      0 <=rseq.0 by A1;
      hence thesis by A6,A9,SEQM_3:5;
    end;
    Partial_Sums(rseq).n1 >0
    proof
      now
        per cases;
        case
A10:      n1=0;
          then Partial_Sums(rseq).n1=rseq.0 by SERIES_1:def 1;
          hence thesis by A1,A7,A10;
        end;
        case
A11:      n1<>0;
          set nn=n1-1;
A12:      nn+1 =n1 & 0 <= rseq.n1 by A1;
          0 <= n1 by NAT_1:2;
          then 0 + 1 <= n1 by A11,INT_1:7;
          then
A13:      nn in NAT by INT_1:5;
          then 0 <= Partial_Sums(rseq).nn by A8;
          then rseq.(n1)+0 <= rseq.(n1)+Partial_Sums(rseq).nn by XREAL_1:7;
          hence thesis by A7,A13,A12,SERIES_1:def 1;
        end;
      end;
      hence thesis;
    end;
    hence contradiction by A3,A5;
  end;
  hence thesis;
end;

registration
  cluster l2_Space -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
  coherence by Th13,Th15;
end;