non empty NORMSTR equals NORMSTR (# the_set_of_l1RealSequences, Zero_(the_set_of_l1RealSequences, Linear_Space_of_RealSequences), Add_(the_set_of_l1RealSequences, Linear_Space_of_RealSequences), Mult_(the_set_of_l1RealSequences, Linear_Space_of_RealSequences), l_norm #); coherence; end; begin :: l1_Space is Banach theorem Th6: the carrier of l1_Space = the_set_of_l1RealSequences & ( for x be set holds x is VECTOR of l1_Space iff x is Real_Sequence & seq_id x is absolutely_summable ) & 0.l1_Space = Zeroseq & ( for u be VECTOR of l1_Space holds u =seq_id u ) & ( for u,v be VECTOR of l1_Space holds u+v =seq_id(u)+ seq_id(v) ) & ( for r be Real for u be VECTOR of l1_Space holds r*u =r(#)seq_id (u) ) & ( for u be VECTOR of l1_Space holds -u = -seq_id u & seq_id(-u) = - seq_id(u) ) & ( for u,v be VECTOR of l1_Space holds u-v =seq_id(u)-seq_id v ) & ( for v be VECTOR of l1_Space holds seq_id v is absolutely_summable ) & for v be VECTOR of l1_Space holds ||.v.|| = Sum abs seq_id v proof set l1 =l1_Space; A1: for x be set holds x is Element of l1 iff x is Real_Sequence & seq_id x is absolutely_summable proof let x be set; x in the_set_of_RealSequences iff x is Real_Sequence by FUNCT_2:8,66; hence thesis by Def1; end; A2: for u,v be VECTOR of l1 holds u+v =seq_id(u)+seq_id(v) proof let u,v be VECTOR of l1; reconsider u1=u, v1=v as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10; set L1=Linear_Space_of_RealSequences; set W = the_set_of_l1RealSequences; dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by FUNCT_2:def 1; then dom ((the addF of Linear_Space_of_RealSequences)||W) =[:W,W:] by RELAT_1:62,ZFMISC_1:96; then A3: [u,v] in dom ((the addF of Linear_Space_of_RealSequences)||W) by ZFMISC_1:87; u+v =((the addF of Linear_Space_of_RealSequences)||W).[u,v] by RSSPACE:def 8 .=u1+v1 by A3,FUNCT_1:47; hence thesis by RSSPACE:2; end; A4: for r be Real for u be VECTOR of l1 holds r*u =r(#)seq_id(u) proof let r be Real; let u be VECTOR of l1; reconsider r as Element of REAL by XREAL_0:def 1; reconsider u1=u as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10; set L1=Linear_Space_of_RealSequences; set W = the_set_of_l1RealSequences; dom (the Mult of L1) = [:REAL,the carrier of L1:] by FUNCT_2:def 1; then dom ((the Mult of Linear_Space_of_RealSequences) | [:REAL,W:]) =[: REAL,W:] by RELAT_1:62,ZFMISC_1:96; then A5: [r,u] in dom ((the Mult of Linear_Space_of_RealSequences)|[:REAL,W :] ) by ZFMISC_1:87; r*u =((the Mult of Linear_Space_of_RealSequences)|[:REAL,W:]).[r,u] by RSSPACE:def 9 .=r*u1 by A5,FUNCT_1:47; hence thesis by RSSPACE:3; end; A6: for u be VECTOR of l1 holds u =seq_id u proof let u be VECTOR of l1; u is VECTOR of Linear_Space_of_RealSequences by Lm1,RLSUB_1:10; hence thesis; end; A7: for u be VECTOR of l1 holds -u =-seq_id u & seq_id(-u)=-seq_id u proof let u be VECTOR of l1; -u = (-1)*u by Th5,RLVECT_1:16 .= (-1)(#)seq_id(u) by A4 .= -seq_id(u) by SEQ_1:17; hence thesis; end; A8: for u,v be VECTOR of l1 holds u-v =seq_id(u)-seq_id(v) proof let u,v be VECTOR of l1; thus u-v = seq_id(u)+seq_id(-v) by A2 .= seq_id(u)+(-seq_id(v)) by A7 .= seq_id(u)-seq_id(v) by SEQ_1:11; end; A9: for v be VECTOR of l1 holds ||.v.|| = Sum abs seq_id v by Def2; 0.l1 = 0.Linear_Space_of_RealSequences by RSSPACE:def 10 .= Zeroseq; hence thesis by A1,A6,A2,A4,A7,A8,A9; end; theorem Th7: for x, y being Point of l1_Space, a be Real holds ( ||.x.|| = 0 iff x = 0.l1_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| & ||. a*x .|| = |.a.| * ||.x.|| proof let x, y be Point of l1_Space; let a be Real; A1: for n be Nat holds 0 <= abs(seq_id x).n proof let n be Nat; 0 <= |.(seq_id x).n.| by COMPLEX1:46; hence thesis by SEQ_1:12; end; A2: now let n be Nat; (abs(seq_id(x+y))).n = |.(seq_id(x+y)).n.| by SEQ_1:12; hence 0 <= (abs(seq_id(x+y))).n by COMPLEX1:46; end; A3: for n be Nat holds (abs seq_id(x+y)).n = |.((seq_id x).n) + ((seq_id y).n).| proof let n be Nat; (abs seq_id(x+y)).n = (abs(seq_id(seq_id(x)+seq_id y))).n by Th6 .= |.(seq_id x+seq_id y).n.| by SEQ_1:12 .= |.((seq_id x).n)+((seq_id y).n).| by SEQ_1:7; hence thesis; end; A4: for n be Nat holds (abs seq_id(x+y)).n <= (abs seq_id x).n + (abs seq_id y).n proof let n be Nat; (|.((seq_id x).n)+ ((seq_id y).n).|) <= |.(seq_id x).n.| + |.( seq_id y).n.| by COMPLEX1:56; then (abs(seq_id(x+y))) .n <= |.(seq_id x).n.| + |.(seq_id y).n.| by A3; then (abs(seq_id(x+y))) .n <= (abs(seq_id x)).n + |.(seq_id y).n.| by SEQ_1:12; hence thesis by SEQ_1:12; end; A5: for n being Nat holds (abs(seq_id(x+y))).n <= ((abs seq_id x ) + (abs seq_id y)).n proof let n be Nat; (abs seq_id x).n + (abs seq_id y).n =((abs seq_id x) + (abs seq_id y) ).n by SEQ_1:7; hence thesis by A4; end; seq_id y is absolutely_summable by Def1; then A6: abs seq_id y is summable by SERIES_1:def 4; seq_id x is absolutely_summable by Def1; then abs seq_id x is summable by SERIES_1:def 4; then (abs seq_id x) + (abs seq_id y) is summable by A6,SERIES_1:7; then A7: Sum(abs(seq_id(x+y))) <= Sum((abs seq_id x) + (abs seq_id y)) by A5,A2, SERIES_1:20; A8: now assume x=0.l1_Space; then A9: for n be Nat holds (seq_id x).n=0 by Th6,RSSPACE:4; thus ||.x.|| = Sum abs seq_id x by Def2 .= 0 by A9,Th3; end; A10: Sum abs seq_id(x+y) = ||.x + y.|| by Th6; A11: now A12: x in the_set_of_RealSequences by Def1; assume A13: ||.x.|| = 0; ||.x.|| = Sum abs seq_id x & seq_id(x) is absolutely_summable by Th6; then for n be Nat holds 0 = (seq_id x).n by A13,Th4; hence x=0.l1_Space by A12,Th6,RSSPACE:5; end; A14: ||.x.|| = Sum abs seq_id x & ||.y.|| = Sum abs seq_id y by Th6; A15: for n be Nat holds (abs(a(#)seq_id(x))).n =|.a.|*(abs( seq_id x).n) proof let n be Nat; (abs(a(#)seq_id(x))).n =|.(a(#)seq_id(x)).n.| by SEQ_1:12 .=|.a*((seq_id x).n).| by SEQ_1:9 .=|.a.|*(|.(seq_id x).n.|) by COMPLEX1:65 .=|.a.|*(abs(seq_id x).n) by SEQ_1:12; hence thesis; end; seq_id x is absolutely_summable by Def1; then A16: abs seq_id x is summable by SERIES_1:def 4; seq_id x is absolutely_summable by Def1; then A17: abs seq_id x is summable by SERIES_1:def 4; ||.(a*x).|| =Sum(abs(seq_id(a*x))) by Th6 .=Sum(|.seq_id(a(#)seq_id(x)).|) by Th6 .=Sum(|.a.| (#) (abs seq_id x)) by A15,SEQ_1:9 .=|.a.|*Sum(abs seq_id x) by A16,SERIES_1:10 .=|.a.|*||.x.|| by Th6; hence thesis by A11,A8,A1,A17,A14,A10,A6,A7,SERIES_1:7,18; end; registration cluster l1_Space -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; coherence by Th7,Lm2,NORMSP_1:def 1,RSSPACE:15; end; Lm3: 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.|+seq1.i) holds rseq is convergent & lim rseq =|.lim seq-c.|+lim seq1 proof let c be Real; let seq,seq1 be Real_Sequence such that A1: seq is convergent and A2: seq1 is convergent; reconsider cc = c as Element of REAL by XREAL_0:def 1; set cseq = seq_const c; A3: seq -cseq is convergent by A1; then A4: abs(seq- cseq) is convergent; let rseq be Real_Sequence such that A5: for i be Nat holds rseq .i = |.seq.i-c.|+seq1.i; now let i be Element of NAT; thus rseq.i=|.seq.i-c.|+seq1.i by A5 .=|.seq.i-cseq.i.|+seq1.i by SEQ_1:57 .=|.seq.i+(-cseq.i).|+seq1.i .=|.seq.i+(-cseq).i.|+seq1.i by SEQ_1:10 .=|.(seq+ -cseq).i.| + seq1.i by SEQ_1:7 .=|.(seq-cseq).i.| + seq1.i by SEQ_1:11 .=abs(seq-cseq).i + seq1.i by SEQ_1:12 .=(abs(seq-cseq) + seq1).i by SEQ_1:7; end; then A6: rseq = (abs(seq-(cseq)) + seq1) by FUNCT_2:63; lim abs(seq-cseq) = |.lim(seq-cseq).| by A3,SEQ_4:14 .= |.lim seq - lim cseq.| by A1,SEQ_2:12 .= |.lim seq - (cseq.0).| by SEQ_4:26 .= |.lim seq - c.| by SEQ_1:57; hence thesis by A2,A6,A4,SEQ_2:6; end; definition let X be non empty NORMSTR, x, y be Point of X; func dist(x,y) -> Real equals ||.x - y.||; coherence; end; reserve NRM for non empty RealNormSpace; reserve seq for sequence of NRM; definition let NRM be non empty NORMSTR; let seqt be sequence of NRM; attr seqt is CCauchy means for r1 be Real st r1 > 0 ex k1 be Nat st for n1, m1 be Nat st n1 >= k1 & m1 >= k1 holds dist(seqt.n1, seqt.m1) < r1; end; notation let NRM be non empty NORMSTR; let seqt be sequence of NRM; synonym seqt is Cauchy_sequence_by_Norm for seqt is CCauchy; end; theorem Th8: seq is Cauchy_sequence_by_Norm iff for r be Real st r > 0 ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.( seq.n) - (seq.m).|| < r proof thus seq is Cauchy_sequence_by_Norm implies for r be Real st r > 0 ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.(seq.n ) - (seq.m).|| < r proof assume A1: seq is Cauchy_sequence_by_Norm; let r be Real; assume r > 0; then consider k be Nat such that A2: for n, m be Nat st n >= k & m >= k holds dist(seq.n, seq.m) < r by A1; for n, m be Nat st n >= k & m >= k holds ||.(seq.n) - (seq. m).|| < r proof let n,m be Nat; assume n >= k & m >= k; then dist(seq.n, seq.m) < r by A2; hence thesis; end; hence thesis; end; assume A3: for r be Real st r > 0 ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.(seq.n) - (seq.m).|| < r; now let r be Real; assume A4: r > 0; now consider k be Nat such that A5: for n, m be Nat st n >= k & m >= k holds ||.(seq.n ) - (seq.m).|| < r by A3,A4; for n,m be Nat st n >= k & m >= k holds dist(seq.n, seq.m) < r by A5; hence ex k be Nat st for n, m be Nat st n >= k & m >= k holds dist(seq.n, seq.m) < r; end; hence ex k be Nat st for n, m be Nat st n >= k & m >= k holds dist(seq.n, seq.m) < r; end; hence thesis; end; theorem for vseq be sequence of l1_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent proof let vseq be sequence of l1_Space such that A1: 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; A2: 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 A3: 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 e be Real such that A4: e > 0; thus ex k be Nat st for m be Nat st k <= m holds |.rseqi.m -rseqi.k.| < e proof consider k be Nat such that A5: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n ) - (vseq.m).|| < e by A1,A4,Th8; for m being Nat st k <= m holds |.rseqi.m-rseqi.k.| < e proof let m be Nat such that A6: k<=m; A7: for i be Nat holds 0 <= |.seq_id((vseq.m) - (vseq. k)).|. i proof let i be Nat; 0 <= |.(seq_id((vseq.m) - (vseq.k))).i.| by COMPLEX1:46; hence thesis by SEQ_1:12; end; seq_id((vseq.m)-(vseq.k)) is absolutely_summable by Def1; then abs(seq_id((vseq.m)-(vseq.k))) is summable by SERIES_1:def 4; then A8: abs(seq_id((vseq.m) - (vseq.k))).i <= Sum(|.seq_id((vseq.m) - (vseq.k)).|) by A7,RSSPACE2:3; seq_id((vseq.m) - (vseq.k)) =seq_id(seq_id((vseq.m))-seq_id(( vseq.k))) by Th6 .= seq_id((vseq.m))+-seq_id((vseq.k)) by SEQ_1:11; then (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 .=(seq_id((vseq.m))).i-(seq_id((vseq.k))).i .=rseqi.m -(seq_id((vseq.k))).i by A3 .=rseqi.m - rseqi.k by A3; then A9: |.rseqi.m-rseqi.k.| = abs(seq_id((vseq.m) - (vseq.k))).i by SEQ_1:12; ||.(vseq.m) - (vseq.k).|| =Sum(|.seq_id((vseq.m) - (vseq.k)).| ) by Th6; then Sum(|.seq_id((vseq.m) - (vseq.k)).|) < e by A5,A6; hence thesis by A8,A9,XXREAL_0:2; end; hence thesis; end; end; then rseqi is convergent by SEQ_4:41; hence thesis by A3; end; consider f be sequence of REAL such that A10: for x be object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A2); reconsider tseq=f as Real_Sequence; A11: now let i be Nat; reconsider x=i as set; i in NAT by ORDINAL1:def 12; then 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 A10; 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; A12: for e be Real st e >0 ex k be Nat st for n be Nat st n >= k holds abs(seq_id tseq-seq_id(vseq.n)) is summable & Sum(abs(seq_id tseq-seq_id(vseq.n))) < e proof let e1 be Real such that A13: e1 >0; reconsider e1 as Real; set e=e1/2; A14: e < e1 by A13,XREAL_1:216; e > 0 by A13,XREAL_1:215; then consider k be Nat such that A15: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) - (vseq.m).|| < e by A1,Th8; A16: for m,n be Nat st n >= k & m >= k holds ( abs(seq_id((vseq .n) - (vseq.m))) is summable & Sum(abs(seq_id((vseq.n) - (vseq.m)))) < e & for i be Nat holds 0 <= abs(seq_id((vseq.n) - (vseq.m))).i ) proof let m,n be Nat; assume n >= k & m >= k; then ||.(vseq.n) - (vseq.m).|| < e by A15; then A17: (the normF of l1_Space).((vseq.n) - (vseq.m)) < e; A18: for i be Nat holds 0 <= abs(seq_id((vseq.n) - (vseq.m))) .i proof let i be Nat; 0 <= |.(seq_id((vseq.n) - (vseq.m))).i.| by COMPLEX1:46; hence thesis by SEQ_1:12; end; seq_id(((vseq.n) - (vseq.m))) is absolutely_summable by Def1; hence thesis by A17,A18,Def2,SERIES_1:def 4; end; A19: for n be Nat for i be Nat holds for rseq be Real_Sequence st ( for m be Nat holds rseq.m=Partial_Sums(abs(seq_id ((vseq.m)-(vseq.n)))).i ) holds rseq is convergent & lim rseq = Partial_Sums( abs(seq_id tseq-seq_id(vseq.n))).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(abs(seq_id((vseq.m) - (vseq.n)))).$1 holds rseq is convergent & lim rseq = Partial_Sums(abs(seq_id tseq-seq_id(vseq. n))).$1; A20: 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 Th6; hence thesis; end; now let i be Nat such that A21: for rseq be Real_Sequence st ( for m be Nat holds rseq.m= Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).i ) holds rseq is convergent & lim rseq = Partial_Sums(abs((seq_id tseq - seq_id(vseq.n)))).i; thus for rseq be Real_Sequence st ( for m be Nat holds rseq .m = Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).(i+1) ) holds rseq is convergent & lim rseq =Partial_Sums(abs((seq_id tseq - seq_id(vseq.n)))).(i+1) proof deffunc F(Nat) = Partial_Sums(abs(seq_id((vseq.$1) - ( vseq.n)))).i; consider rseqb be Real_Sequence such that A22: for m be Nat holds rseqb.m = F(m) from SEQ_1:sch 1; consider rseq0 be Real_Sequence such that A23: for m be Nat holds rseq0.m=(seq_id(vseq.m)).(i+1 ) and A24: rseq0 is convergent and A25: tseq.(i+1)=lim rseq0 by A11; let rseq be Real_Sequence such that A26: for m be Nat holds rseq.m = Partial_Sums(abs( seq_id((vseq.m) - (vseq.n)))).(i+1); A27: now let m be Nat; thus rseq.m = Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).(i+1) by A26 .=abs(seq_id((vseq.m) - (vseq.n))).(i+1) +Partial_Sums(abs( seq_id((vseq.m) - (vseq.n)))).i by SERIES_1:def 1 .=abs(seq_id(vseq.m)-seq_id(vseq.n)).(i+1) +Partial_Sums(abs( seq_id((vseq.m) - (vseq.n)))).i by A20 .=abs(seq_id(vseq.m)-seq_id(vseq.n)).(i+1) + rseqb.m by A22 .=|.(seq_id(vseq.m)-seq_id(vseq.n)).(i+1).| + rseqb.m by SEQ_1:12 .=|.(seq_id(vseq.m)+-seq_id(vseq.n)).(i+1).| + rseqb.m by SEQ_1:11 .=|.(seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1).| + rseqb. m by SEQ_1:7 .=|.(seq_id(vseq.m)).(i+1)+-(seq_id(vseq.n)).(i+1).| + rseqb. m by SEQ_1:10 .= |.(seq_id(vseq.m)).(i+1)-(seq_id(vseq.n)).(i+1).| + rseqb. m .= |.rseq0.m-(seq_id(vseq.n)).(i+1).| + rseqb.m by A23; end; A28: rseqb is convergent by A21,A22; then lim rseq = |.lim(rseq0)-(seq_id(vseq.n)).(i+1).| + lim rseqb by A24,A27,Lm3 .= |.tseq.(i+1)+-(seq_id(vseq.n)).(i+1).| + lim rseqb by A25 .= |.tseq.(i+1)+(-seq_id(vseq.n)).(i+1).| + lim rseqb by SEQ_1:10 .= |.(tseq+(-seq_id(vseq.n))).(i+1).| + lim rseqb by SEQ_1:7 .= |.(tseq-(seq_id(vseq.n))).(i+1).| + lim rseqb by SEQ_1:11 .= abs(tseq-(seq_id(vseq.n))).(i+1) + lim rseqb by SEQ_1:12 .= abs(tseq-(seq_id(vseq.n))).(i+1) + Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))).i by A21,A22 .= Partial_Sums (abs((seq_id tseq -seq_id(vseq.n)))).(i+1) by SERIES_1:def 1; hence thesis by A28,A24,A27,Lm3; end; end; then A29: for i be Nat st P[i] holds P[i+1]; now let rseq be Real_Sequence such that A30: for m be Nat holds rseq.m=Partial_Sums(abs(seq_id( (vseq.m) - (vseq.n)))).0; thus rseq is convergent & lim rseq = Partial_Sums(abs(seq_id tseq- seq_id(vseq.n))).0 proof consider rseq0 be Real_Sequence such that A31: for m be Nat holds rseq0.m=(seq_id(vseq.m)).0 and A32: rseq0 is convergent and A33: tseq.0=lim rseq0 by A11; A34: for m being Nat holds rseq.m = |.rseq0.m-(seq_id(( vseq.n))).0 .| proof let m be Nat; rseq.m=Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).0 by A30 .=(abs(seq_id((vseq.m) - (vseq.n)))).0 by SERIES_1:def 1 .=(abs(seq_id(vseq.m)-seq_id(vseq.n))).0 by A20 .=(abs(seq_id(vseq.m)+-seq_id(vseq.n))).0 by SEQ_1:11 .=|.(seq_id(vseq.m)+-seq_id(vseq.n)).0 .| by SEQ_1:12 .=|.(seq_id(vseq.m)).0+(-seq_id(vseq.n)).0 .| by SEQ_1:7 .=|.(seq_id(vseq.m)).0+-(seq_id(vseq.n)).0 .| by SEQ_1:10 .=|.(seq_id(vseq.m)).0-(seq_id(vseq.n)).0 .|; hence thesis by A31; end; then lim rseq = |.lim(rseq0) -((seq_id(vseq.n)).0 ).| by A32,Th1 .= |.tseq.0+-((seq_id(vseq.n)).0).| by A33 .= |.tseq.0+(-(seq_id(vseq.n))).0 .| by SEQ_1:10 .= |.(tseq+(-seq_id((vseq.n)))).0 .| by SEQ_1:7 .= |.(tseq-(seq_id((vseq.n)))).0 .| by SEQ_1:11 .= abs(seq_id tseq-(seq_id(vseq.n))).0 by SEQ_1:12 .=Partial_Sums(abs(seq_id tseq-(seq_id(vseq.n)))).0 by SERIES_1:def 1; hence thesis by A32,A34,Th1; end; end; then A35: P[0]; for i be Nat holds P[i] from NAT_1:sch 2(A35,A29); hence thesis; end; for n be Nat st n >= k holds abs(seq_id tseq-seq_id(vseq.n )) is summable & Sum abs(seq_id tseq-seq_id(vseq.n)) < e1 proof let n be Nat such that A36: n >= k; A37: for i be Nat st 0 <= i holds Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))).i <=e proof let i be Nat such that 0 <=i; deffunc F(Nat)= Partial_Sums(abs(seq_id((vseq.$1) - (vseq.n )))).i; consider rseq be Real_Sequence such that A38: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1; A39: for m be Nat st m >= k holds rseq.m <= e proof let m be Nat; A40: rseq.m = Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).i by A38; assume A41: m >= k; then abs(seq_id((vseq.m) - (vseq.n))) is summable & for i be Nat holds 0 <= abs(seq_id((vseq.m) - (vseq.n))).i by A16,A36; then A42: Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).i <=Sum(abs( seq_id((vseq.m) - (vseq.n)))) by RSSPACE2:3; Sum(abs(seq_id((vseq.m) - (vseq.n)))) < e by A16,A36,A41; hence thesis by A42,A40,XXREAL_0:2; end; rseq is convergent & lim rseq = Partial_Sums(abs(seq_id tseq- seq_id(vseq.n)) ).i by A19,A38; hence thesis by A39,RSSPACE2:5; end; now take e1; let i be Nat; Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))).i <=e by A37,NAT_1:2; hence Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))).i < e1 by A14, XXREAL_0:2; end; then A43: Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))) is bounded_above by SEQ_2:def 3; A44: for i be Nat holds 0 <= abs(seq_id tseq-seq_id(vseq.n)). i proof let i be Nat; abs(seq_id tseq -seq_id(vseq.n)).i =|.(seq_id tseq -seq_id(vseq .n)).i.| by SEQ_1:12; hence thesis by COMPLEX1:46; end; then abs((seq_id tseq-seq_id(vseq.n))) is summable by A43,SERIES_1:17; then Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))) is convergent by SERIES_1:def 2; then Sum(abs((seq_id tseq -seq_id(vseq.n)))) = lim Partial_Sums(abs(( seq_id tseq - seq_id(vseq.n)))) & lim Partial_Sums(abs((seq_id tseq -seq_id( vseq.n)))) <= e by A37,RSSPACE2:5,SERIES_1:def 3; hence thesis by A14,A44,A43,SERIES_1:17,XXREAL_0:2; end; hence thesis; end; abs seq_id tseq is summable proof set d=abs seq_id tseq; A45: for i be Nat holds 0 <= abs(seq_id tseq).i proof let i be Nat; abs(seq_id tseq).i = |.(seq_id tseq).i.| by SEQ_1:12; hence thesis by COMPLEX1:46; end; consider m be Nat such that A46: for n be Nat st n >= m holds abs((seq_id tseq -seq_id( vseq.n))) is summable & Sum(abs((seq_id tseq -seq_id(vseq.n)))) < 1 by A12; set b=abs seq_id(vseq.m); set a=abs(seq_id tseq -seq_id(vseq.m)); seq_id(vseq.m) is absolutely_summable by Def1; then A47: abs(seq_id(vseq.m)) is summable by SERIES_1:def 4; A48: for i be Nat holds d.i <= (a+b).i proof let i be Nat; A49: b.i=|.(seq_id(vseq.m)).i.| & d.i=|.(seq_id tseq).i.| by SEQ_1:12; a.i = |.(seq_id tseq -seq_id(vseq.m)).i.| by SEQ_1:12 .= |.(seq_id tseq+-seq_id(vseq.m)).i.| by SEQ_1:11 .= |.(seq_id tseq).i+(-seq_id(vseq.m)).i.| by SEQ_1:7 .= |.(seq_id tseq).i+(-(seq_id(vseq.m)).i).| by SEQ_1:10 .=|.(seq_id tseq).i-(seq_id(vseq.m)).i.|; then d.i-b.i <= a.i by A49,COMPLEX1:59; then d.i-b.i+b.i<= a.i + b.i by XREAL_1:6; hence thesis by SEQ_1:7; end; abs((seq_id tseq -seq_id(vseq.m))) is summable by A46; then a + b is summable by A47,SERIES_1:7; hence thesis by A45,A48,SERIES_1:20; end; then A50: seq_id tseq is absolutely_summable by SERIES_1:def 4; A51: tseq in the_set_of_RealSequences by FUNCT_2:8; then reconsider tv=tseq as Point of l1_Space by A50,Def1; 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; assume e > 0; then consider m be Nat such that A52: for n be Nat st n >= m holds abs(seq_id tseq-seq_id( vseq.n)) is summable & Sum(abs(seq_id tseq-seq_id(vseq.n))) < e by A12; reconsider m as Element of NAT by ORDINAL1:def 12; take m; reconsider u=tseq as VECTOR of l1_Space by A50,A51,Def1; let n be Nat; assume n >= m; then A53: Sum abs(seq_id tseq-seq_id(vseq.n)) < e by A52; reconsider v=vseq.n as VECTOR of l1_Space; seq_id(u-v) = u-v by Th6; then Sum abs seq_id(u-v) = Sum abs(seq_id tseq-seq_id(vseq.n)) by Th6; then A54: (the normF of l1_Space).(u-v) < e by A53,Def2; ||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33 .=||.tv-(vseq.n).|| by NORMSP_1:2; hence ||.(vseq.n) - tv.|| < e by A54; end; hence thesis by NORMSP_1:def 6; end;