:: Banach Space of Absolute Summable Complex Sequences
:: by Noboru Endou
::
:: Received February 24, 2004
:: Copyright (c) 2004-2026 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, SUBSET_1, CSSPACE, RSSPACE, SERIES_1, TARSKI, XCMPLX_0,
COMSEQ_1, SEQ_1, SEQ_2, FUNCT_1, COMPLEX1, ARYTM_1, ORDINAL2, FUNCOP_1,
ARYTM_3, XBOOLE_0, RLSUB_1, RLVECT_1, CARD_1, XXREAL_0, RELAT_1,
VALUED_1, CLVECT_1, ALGSTR_0, CARD_3, BINOP_1, ZFMISC_1, STRUCT_0,
SUPINF_2, NORMSP_1, REALSET1, PRE_TOPC, METRIC_1, REAL_1, NAT_1,
RSSPACE3, XXREAL_2, CSSPACE3, NORMSP_0, RELAT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0,
XCMPLX_0, COMPLEX1, NAT_1, STRUCT_0, ALGSTR_0, RELAT_1, BINOP_1,
REALSET1, DOMAIN_1, PARTFUN1, FUNCT_1, XXREAL_0, FUNCT_2, FUNCOP_1,
PRE_TOPC, RLVECT_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, COMSEQ_1, COMSEQ_2,
COMSEQ_3, NORMSP_0, CLVECT_1, CSSPACE;
constructors BINOP_1, FUNCOP_1, REAL_1, COMSEQ_2, COMSEQ_3, REALSET1, CSSPACE,
SEQ_2, RELSET_1, CFUNCDOM;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
XREAL_0, MEMBERED, COMSEQ_2, REALSET1, STRUCT_0, CLVECT_1, CSSPACE,
VALUED_1, VALUED_0, XCMPLX_0, SEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0, CSSPACE,
CFUNCDOM;
expansions NORMSP_0;
theorems RELAT_1, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SERIES_1, FUNCT_1, NAT_1,
FUNCT_2, RLVECT_1, CSSPACE, CLVECT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3,
COMPLEX1, TARSKI, XBOOLE_0, RSSPACE2, FUNCOP_1, XREAL_1, XXREAL_0,
VALUED_1, XCMPLX_0, XREAL_0, CSSPACE2, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, COMSEQ_1, XBOOLE_0;
begin :: Complex_l1_Space:The Space of Absolute Summable Complex Sequences
definition
func the_set_of_l1ComplexSequences -> Subset of
Linear_Space_of_ComplexSequences means
:Def1:
for x being object holds x in it iff
x in the_set_of_ComplexSequences & seq_id(x) is absolutely_summable;
existence
proof
defpred P[object] means seq_id($1) is absolutely_summable;
consider IT being set such that
A1: for x being object holds x in IT iff x in the_set_of_ComplexSequences
& P[x] from XBOOLE_0:sch 1;
for x be object st x in IT holds x in the_set_of_ComplexSequences by A1;
then IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of Linear_Space_of_ComplexSequences;
assume that
A2: for x being object holds x in X1 iff x in the_set_of_ComplexSequences
& seq_id(x) is absolutely_summable and
A3: for x being object holds x in X2 iff x in the_set_of_ComplexSequences
& seq_id(x) is absolutely_summable;
for x being object st x in X2 holds x in X1
proof
let x be object;
assume x in X2;
then
x in the_set_of_ComplexSequences & seq_id(x) is absolutely_summable
by A3;
hence thesis by A2;
end;
then
A4: X2 c= X1 by TARSKI:def 3;
for x being object st x in X1 holds x in X2
proof
let x be object;
assume x in X1;
then
x in the_set_of_ComplexSequences & seq_id(x) is absolutely_summable
by A2;
hence thesis by A3;
end;
then X1 c= X2 by TARSKI:def 3;
hence thesis by A4,XBOOLE_0:def 10;
end;
end;
theorem Th1:
for c be Complex, seq be Complex_Sequence, rseq be Real_Sequence
st seq is convergent & ( for i be Nat holds rseq.i = |.(seq.i-c).| )
holds rseq is convergent & lim rseq = |.(lim seq-c).|
proof
let c be Complex;
let seq be Complex_Sequence;
let rseq be Real_Sequence;
assume that
A1: seq is convergent and
A2: for i be Nat holds rseq.i = |.(seq.i-c).|;
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider cseq = NAT --> c1 as Complex_Sequence;
A3: for n be Nat holds cseq.n=c
by ORDINAL1:def 12,FUNCOP_1:7;
then
A4: cseq is convergent by COMSEQ_2:9;
then reconsider seq9 = seq-cseq as convergent Complex_Sequence by A1;
seq -cseq is convergent by A1,A4;
then
A5: lim |.(seq -cseq).| = |.(lim(seq-cseq)).| by SEQ_2:27
.=|.(lim seq-lim cseq).| by A1,A4,COMSEQ_2:26
.=|.(lim seq-c).| by A3,COMSEQ_2:10;
now
let i be Nat;
A6: i in NAT by ORDINAL1:def 12;
thus rseq.i=|.(seq.i-c).| by A2
.=|.(seq.i-(cseq.i)).|by FUNCOP_1:7,A6
.=|.(seq.i+-(cseq.i)).|
.=|.(seq.i+(-cseq).i).| by VALUED_1:8
.=|.(seq -cseq).i .| by VALUED_1:1,A6
.=|. seq-cseq .| .i by VALUED_1:18;
end;
then
A7: for x be object st x in NAT holds rseq.x = |.(seq -cseq).| .x;
|.seq9.| is convergent;
hence thesis by A7,A5,FUNCT_2:12;
end;
registration
cluster the_set_of_l1ComplexSequences -> non empty;
coherence
proof
seq_id CZeroseq is absolutely_summable
proof
reconsider cseq=seq_id CZeroseq as Complex_Sequence;
for n being Nat holds cseq.n = 0c by CSSPACE:4;
hence thesis by COMSEQ_3:51;
end;
hence thesis by Def1;
end;
end;
registration
cluster the_set_of_l1ComplexSequences -> linearly-closed;
coherence
proof
set W = the_set_of_l1ComplexSequences;
A1: for v,u be VECTOR of Linear_Space_of_ComplexSequences st v in
the_set_of_l1ComplexSequences & u in the_set_of_l1ComplexSequences holds v + u
in the_set_of_l1ComplexSequences
proof
let v,u be VECTOR of Linear_Space_of_ComplexSequences such that
A2: v in W and
A3: u in W;
seq_id(v+u) is absolutely_summable
proof
set r = |.seq_id(v+u).|;
set q = |.seq_id u.|;
set p = |.seq_id v.|;
A4: for n be Nat holds 0<=r.n
proof
let n be Nat;
r.n=|.((seq_id(v+u)).n).| by VALUED_1:18;
hence thesis by COMPLEX1:46;
end;
A5: for n be Nat holds r.n <=(p+q).n
proof
let n be Nat;
A6: n in NAT by ORDINAL1:def 12;
A7: |.((seq_id v).n).|+|.((seq_id u).n).| = |.(seq_id v).| .n + |.(
(seq_id u).n).| by VALUED_1:18
.= |.(seq_id v).| .n+ |.(seq_id u).| .n by VALUED_1:18
.= (p + q).n by SEQ_1:7;
r.n=|.((seq_id(v+u)).n).| by VALUED_1:18
.=|.((seq_id(seq_id(v) + seq_id(u))).n).| by CSSPACE:2
.=|.((seq_id v).n + (seq_id u).n).| by VALUED_1:1,A6;
hence thesis by A7,COMPLEX1:56;
end;
seq_id u is absolutely_summable by A3,Def1;
then
A8: q is summable by COMSEQ_3:def 9;
seq_id v is absolutely_summable by A2,Def1;
then p is summable by COMSEQ_3:def 9;
then p+q is summable by A8,SERIES_1:7;
then r is summable by A4,A5,SERIES_1:20;
hence thesis by COMSEQ_3:def 9;
end;
hence thesis by Def1;
end;
for a be Complex, v be VECTOR of Linear_Space_of_ComplexSequences st
v in W holds a * v in W
proof
let a be Complex;
let v be VECTOR of Linear_Space_of_ComplexSequences such that
A9: v in W;
seq_id(a*v) is absolutely_summable
proof
set r1 = ((|.a.|)(#)|.(seq_id v).|);
set q1 = |.seq_id(a*v).|;
A10: for n be Nat holds 0<=q1.n
proof
let n be Nat;
q1.n=|.((seq_id(a*v)).n).| by VALUED_1:18;
hence thesis by COMPLEX1:46;
end;
A11: for n be Nat holds q1.n <=r1.n
proof
let n be Nat;
q1.n=|.((seq_id(a*v)).n).| by VALUED_1:18
.=|.((seq_id(a(#)seq_id v)).n).| by CSSPACE:3
.=|.(a(#)seq_id v).| .n by VALUED_1:18;
hence thesis by COMSEQ_1:50;
end;
seq_id v is absolutely_summable by A9,Def1;
then |. seq_id v .| is summable by COMSEQ_3:def 9;
then r1 is summable by SERIES_1:10;
then q1 is summable by A10,A11,SERIES_1:20;
hence thesis by COMSEQ_3:def 9;
end;
hence thesis by Def1;
end;
hence thesis by A1,CLVECT_1:def 7;
end;
end;
Lm1: CLSStruct (# the_set_of_l1ComplexSequences, Zero_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences) #) is Subspace
of Linear_Space_of_ComplexSequences by CSSPACE:11;
registration
cluster CLSStruct (# the_set_of_l1ComplexSequences, Zero_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences) #) -> Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by CSSPACE:11;
end;
definition
func cl_norm -> Function of the_set_of_l1ComplexSequences, REAL means
:Def2:
for x be object st x in the_set_of_l1ComplexSequences
holds it.x = Sum |.seq_id x.|;
existence
proof
deffunc F(object) = Sum |.seq_id $1.|;
A1: for z be object st z in the_set_of_l1ComplexSequences
holds F(z) in REAL
by XREAL_0:def 1;
ex f being Function of the_set_of_l1ComplexSequences,REAL st for x being
object st x in the_set_of_l1ComplexSequences 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_l1ComplexSequences, REAL such
that
A2: for x be object st x in the_set_of_l1ComplexSequences holds NORM1.x =
Sum |.seq_id x.| and
A3: for x be object st x in the_set_of_l1ComplexSequences holds NORM2.x =
Sum |.seq_id x.|;
A4: for z be object st z in the_set_of_l1ComplexSequences
holds NORM1.z = NORM2. z
proof
let z be object such that
A5: z in the_set_of_l1ComplexSequences;
NORM1.z = Sum |.seq_id z.| by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = the_set_of_l1ComplexSequences & dom NORM2 =
the_set_of_l1ComplexSequences by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
end;
registration
let X be non empty set, Z be Element of X, A be BinOp of X, M be Function of
[:COMPLEX, X:], X, N be Function of X, REAL;
cluster CNORMSTR (# X, Z, A, M, N #) -> non empty;
coherence;
end;
theorem
for l be CNORMSTR st the CLSStruct of l is ComplexLinearSpace holds l
is ComplexLinearSpace by CSSPACE:79;
theorem Th3:
for cseq be Complex_Sequence st (for n be Nat holds
cseq.n=0c) holds cseq is absolutely_summable & Sum |.cseq.| = 0
proof
let cseq be Complex_Sequence such that
A1: for n be Nat holds cseq.n=0c;
A2: for n be Nat holds (|.cseq.|).n=0
proof
let n be Nat;
cseq.n=0c by A1;
hence thesis by COMPLEX1:44,VALUED_1:18;
end;
A3: for m be Nat holds Partial_Sums (|.cseq.|).m = 0
proof
defpred P[Nat] means
(|.cseq.|).$1 = (Partial_Sums |.cseq.|).$1;
let m be Nat;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: (|.cseq.|).k = (Partial_Sums (|.cseq.|)).k;
thus (|.cseq.|).(k+1) = 0 + (|.cseq.|).(k+1)
.= (|.cseq.|).k + (|.cseq.|).(k+1) by A2
.= (Partial_Sums |.cseq.|).(k+1) by A5,SERIES_1:def 1;
end;
A6: P[0] by SERIES_1:def 1;
for n be Nat holds P[n] from NAT_1:sch 2(A6,A4);
hence (Partial_Sums |.cseq.|).m = (|.cseq.|).m .= 0 by A2;
end;
A7: for p be Real st 0<p ex n be Nat st
for m be Nat st n<=m holds |.(Partial_Sums |.cseq.|).m-0 .|<p
proof
let p be Real such that
A8: 0<p;
take 0;
let m be Nat such that
0<=m;
|.(Partial_Sums |.cseq.|).m-0 .| = |.0-0 .| by A3
.= 0 by ABSVALUE:def 1;
hence thesis by A8;
end;
then
A9: Partial_Sums |.cseq.| is convergent by SEQ_2:def 6;
then
A10: |.cseq.| is summable by SERIES_1:def 2;
lim Partial_Sums |.cseq.| =0 by A7,A9,SEQ_2:def 7;
hence thesis by A10,COMSEQ_3:def 9,SERIES_1:def 3;
end;
Lm2: CLSStruct (# the_set_of_l1ComplexSequences, Zero_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences) #) is
ComplexLinearSpace;
definition
func Complex_l1_Space -> non empty CNORMSTR equals
CNORMSTR (#
the_set_of_l1ComplexSequences, Zero_(the_set_of_l1ComplexSequences,
Linear_Space_of_ComplexSequences), Add_(the_set_of_l1ComplexSequences,
Linear_Space_of_ComplexSequences), Mult_(the_set_of_l1ComplexSequences,
Linear_Space_of_ComplexSequences), cl_norm #);
coherence;
end;
::$CT
theorem Th4:
Complex_l1_Space is ComplexLinearSpace by Lm2,CSSPACE:79;
begin :: Complex_l1_Space is Banach
theorem Th5:
the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences &
( for x be set holds x is VECTOR of Complex_l1_Space iff x is Complex_Sequence
& seq_id x is absolutely_summable ) & 0.Complex_l1_Space = CZeroseq & ( for u
be VECTOR of Complex_l1_Space holds u =seq_id u ) & ( for u,v be VECTOR of
Complex_l1_Space holds u+v =seq_id(u)+seq_id(v) ) & ( for p be Complex for u be
VECTOR of Complex_l1_Space holds p*u =p(#)seq_id(u) ) & ( for u be VECTOR of
Complex_l1_Space holds -u = -seq_id u & seq_id(-u) = -seq_id(u) ) & ( for u,v
be VECTOR of Complex_l1_Space holds u-v =seq_id(u)-seq_id v ) & ( for v be
VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & for v be
VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.seq_id v.|
proof
set l1 =Complex_l1_Space;
A1: for x be set holds x is Element of l1 iff x is Complex_Sequence & seq_id
x is absolutely_summable
proof
let x be set;
x in the_set_of_ComplexSequences iff x is Complex_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_ComplexSequences by Lm1,
CLVECT_1:29;
set L1=Linear_Space_of_ComplexSequences;
set W = the_set_of_l1ComplexSequences;
dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by
FUNCT_2:def 1;
then
A3: dom ((the addF of Linear_Space_of_ComplexSequences)||W) =[:W,W:] by
RELAT_1:62,ZFMISC_1:96;
u+v =((the addF of Linear_Space_of_ComplexSequences)||W).[u,v] by
CSSPACE:def 8
.=u1+v1 by A3,FUNCT_1:47;
hence thesis by CSSPACE:2;
end;
A4: for p be Complex for u be VECTOR of l1 holds p*u =p(#)seq_id(u)
proof
let p be Complex;
let u be VECTOR of l1;
reconsider u1=u as VECTOR of Linear_Space_of_ComplexSequences by Lm1,
CLVECT_1:29;
set L1=Linear_Space_of_ComplexSequences;
set W = the_set_of_l1ComplexSequences;
dom (the Mult of L1) = [:COMPLEX,the carrier of L1:] by FUNCT_2:def 1;
then
A5: dom ((the Mult of Linear_Space_of_ComplexSequences) | [:COMPLEX,W :])
=[:COMPLEX,W:] by RELAT_1:62,ZFMISC_1:96;
reconsider p as Element of COMPLEX by XCMPLX_0:def 2;
p*u =(the Mult of l1).[p,u] by CLVECT_1:def 1
.=((the Mult of Linear_Space_of_ComplexSequences)|[:COMPLEX,W:]).[p,u]
by CSSPACE:def 9
.=(the Mult of Linear_Space_of_ComplexSequences).[p,u] by A5,FUNCT_1:47
.=p*u1 by CLVECT_1:def 1;
hence thesis by CSSPACE: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_ComplexSequences by Lm1,CLVECT_1:29;
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 = (-1r)*u by Th4,CLVECT_1:3
.= (-1r)(#)seq_id(u) by A4
.= -seq_id(u) by COMSEQ_1:11;
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;
end;
A9: for v be VECTOR of l1 holds ||.v.|| = Sum |.seq_id v.|
by Def2;
0.l1 = 0.Linear_Space_of_ComplexSequences by CSSPACE:def 10
.= CZeroseq;
hence thesis by A1,A6,A2,A4,A7,A8,A9;
end;
theorem Th6:
for x, y being Point of Complex_l1_Space, p be Complex holds (
||.x.|| = 0 iff x = 0.Complex_l1_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.||
+ ||.y.|| & ||. p*x .|| = |.p.| * ||.x.||
proof
let x, y be Point of Complex_l1_Space;
let p be Complex;
A1: for n be Nat holds 0 <= (|.seq_id x.|).n
proof
let n be Nat;
0 <= |.((seq_id x).n).| by COMPLEX1:46;
hence thesis by VALUED_1:18;
end;
A2: now
let n be Nat;
(|.seq_id(x+y).|).n = |.((seq_id(x+y)).n).| by VALUED_1:18;
hence 0 <= (|.seq_id(x+y).|).n by COMPLEX1:46;
end;
A3: for n be Nat holds (|.seq_id(x+y).|).n = |.(((seq_id x).n) +
((seq_id y).n)).|
proof
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
(|.seq_id(x+y).|).n = (|.(seq_id(seq_id(x)+seq_id y)).|).n by Th5
.= |.((seq_id x+seq_id y).n).| by VALUED_1:18
.= |.(((seq_id x).n)+((seq_id y).n)).| by VALUED_1:1,A4;
hence thesis;
end;
A5: for n be Nat holds (|.seq_id(x+y).|).n <= (|.seq_id x.|).n +
(|.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 (|.(seq_id(x+y)).|) .n <= |.((seq_id x).n).| + |.((seq_id y).n).| by
A3;
then (|.(seq_id(x+y)).|) .n <= (|.(seq_id x).|).n + |.((seq_id y).n).| by
VALUED_1:18;
hence thesis by VALUED_1:18;
end;
A6: for n being Nat holds (|.seq_id(x+y).|).n <= (|.seq_id x.| +
|.seq_id y.|).n
proof
let n be Nat;
(|.seq_id x.|).n + (|.seq_id y.|).n =((|.seq_id x.|) + (|.seq_id y.|)
).n by SEQ_1:7;
hence thesis by A5;
end;
seq_id y is absolutely_summable by Def1;
then
A7: |.seq_id y.| is summable by COMSEQ_3:def 9;
seq_id x is absolutely_summable by Def1;
then |.seq_id x.| is summable by COMSEQ_3:def 9;
then |.seq_id x.| + |.seq_id y.| is summable by A7,SERIES_1:7;
then
A8: Sum(|.seq_id(x+y).|) <= Sum(|.seq_id x.| + |.seq_id y.|) by A6,A2,
SERIES_1:20;
A9: now
assume x=0.Complex_l1_Space;
then
A10: for n be Nat holds (seq_id x).n=0 by Th5,CSSPACE:4;
thus ||.x.|| = Sum |.seq_id x.| by Def2
.= 0 by A10,Th3;
end;
A11: Sum |.seq_id(x+y).| = ||.x + y.|| by Th5;
A12: now
A13: x in the_set_of_ComplexSequences by Def1;
assume
A14: ||.x.|| = 0;
||.x.|| = Sum |.seq_id x.| & seq_id(x) is absolutely_summable by Th5;
then for n be Nat holds 0 = (seq_id x).n by A14,CSSPACE2:13;
hence x=0.Complex_l1_Space by A13,Th5,CSSPACE:5;
end;
A15: ||.x.|| = Sum |.seq_id x.| & ||.y.|| = Sum |.seq_id y.| by Th5;
A16: for n be Nat holds (|.p(#)seq_id(x).|).n =|.p.|*(|.seq_id x
.| .n)
proof
let n be Nat;
reconsider p as Element of COMPLEX by XCMPLX_0:def 2;
(|.(p(#)seq_id(x)).|).n =|.((p(#)seq_id(x)).n).| by VALUED_1:18
.=|.(p*((seq_id x).n)).| by VALUED_1:6
.=(|.p.|)*(|.((seq_id x).n).|) by COMPLEX1:65
.=(|.p.|)*((|.seq_id x.|).n) by VALUED_1:18;
hence thesis;
end;
seq_id x is absolutely_summable by Def1;
then
A17: |.seq_id x.| is summable by COMSEQ_3:def 9;
seq_id x is absolutely_summable by Def1;
then
A18: |.seq_id x.| is summable by COMSEQ_3:def 9;
||.(p*x).|| =Sum(|.seq_id(p*x).|) by Th5
.=Sum(|.seq_id(p(#)seq_id(x)).|) by Th5
.=Sum(|.p.|(#)|.seq_id x.|) by A16,SEQ_1:9
.=|.p.|*Sum(|.seq_id x.|) by A17,SERIES_1:10
.=|.p.|*||.x.|| by Th5;
hence thesis by A12,A9,A1,A18,A15,A11,A7,A8,SERIES_1:7,18;
end;
registration
cluster Complex_l1_Space -> reflexive discerning ComplexNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence
by Lm2,Th6,CLVECT_1:def 13,CSSPACE:79;
end;
Lm3: for c be Complex, seq be Complex_Sequence, 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 Complex;
let seq be Complex_Sequence;
let seq1 be Real_Sequence;
assume that
A1: seq is convergent and
A2: seq1 is convergent;
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider cseq = NAT --> c1 as Complex_Sequence;
A3: for n be Nat holds cseq.n=c
by ORDINAL1:def 12,FUNCOP_1:7;
then
A4: lim cseq = c by COMSEQ_2:10
.= cseq.0 by FUNCOP_1:7;
A5: cseq is convergent by A3,COMSEQ_2:9;
then seq -cseq is convergent by A1;
then
A6: lim |.(seq-cseq).| = |.(lim(seq-cseq)).| by SEQ_2:27
.= |.(lim seq - (cseq.0)).| by A1,A4,A5,COMSEQ_2:26
.= |.(lim seq - c).| by FUNCOP_1:7;
let rseq be Real_Sequence such that
A7: 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 A7
.=|.(seq.i-cseq.i).|+seq1.i by FUNCOP_1:7
.=|.(seq.i+(-cseq.i)).|+seq1.i
.=|.(seq.i+(-cseq).i).|+seq1.i by VALUED_1:8
.=|.((seq-cseq).i).| + seq1.i by VALUED_1:1
.=|.(seq-cseq).| .i + seq1.i by VALUED_1:18
.=(|.(seq-cseq).| + seq1).i by SEQ_1:7;
end;
then
A8: rseq = (|.(seq-(cseq)).| + seq1) by FUNCT_2:63;
reconsider seq1=seq-cseq as convergent Complex_Sequence by A1,A5;
|.seq1.| is convergent;
hence thesis by A2,A8,A6,SEQ_2:6;
end;
definition
let X be non empty CNORMSTR, x, y be Point of X;
func dist(x,y) -> Real equals
||.x - y.||;
coherence;
end;
definition
let CNRM be non empty CNORMSTR;
let seqt be sequence of CNRM;
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 CNRM be non empty CNORMSTR;
let seq be sequence of CNRM;
synonym seq is Cauchy_sequence_by_Norm for seq is CCauchy;
end;
reserve NRM for non empty ComplexNormSpace;
reserve seq for sequence of NRM;
theorem Th7:
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;
thus (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) implies seq is
Cauchy_sequence_by_Norm
proof
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 being 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;
end;
theorem
for vseq be sequence of Complex_l1_Space st vseq is
Cauchy_sequence_by_Norm holds vseq is convergent
proof
let vseq be sequence of Complex_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
Complex_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 COMPLEX & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Element of NAT;
deffunc F(Nat) = (seq_id(vseq.$1)).i;
consider rseqi be Complex_Sequence such that
A3: for n be Nat holds rseqi.n= F(n) from COMSEQ_1:sch 1;
take lim rseqi;
thus lim rseqi in COMPLEX by XCMPLX_0:def 2;
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,Th7;
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 VALUED_1:18;
end;
seq_id((vseq.m)-(vseq.k)) is absolutely_summable by Def1;
then |.(seq_id((vseq.m)-(vseq.k))).| is summable by COMSEQ_3:def 9;
then
A8: |.(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 Th5
.= seq_id((vseq.m))+-seq_id((vseq.k));
then
(seq_id((vseq.m) - (vseq.k))).i =(seq_id((vseq.m))).i+(-seq_id(
(vseq.k))).i by VALUED_1:1
.=(seq_id((vseq.m))).i+(-(seq_id((vseq.k))).i) by VALUED_1:8
.=(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).| = |.(seq_id((vseq.m) - (vseq.k))).| .i by
VALUED_1:18;
||.(vseq.m) - (vseq.k).|| =Sum(|.(seq_id((vseq.m) - (vseq.k)))
.|) by Th5;
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 COMSEQ_3:46;
hence thesis by A3;
end;
consider f be sequence of COMPLEX 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 Complex_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 Complex_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 Complex_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 |.(seq_id tseq-seq_id(vseq.n)).| is summable & Sum(|.(seq_id
tseq-seq_id(vseq.n)).|) < e
proof
let e1 be Real such that
A13: e1 >0;
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,Th7;
A16: for m,n be Nat st n >= k & m >= k holds ( |.(seq_id((vseq.
n) - (vseq.m))).| is summable & Sum(|.(seq_id((vseq.n) - (vseq.m))).|) < e &
for i be Nat holds 0 <= |.(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 Complex_l1_Space).(vseq.n-vseq.m) < e;
A18: for i be Nat holds 0 <= |.(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 VALUED_1:18;
end;
seq_id(vseq.n-vseq.m) is absolutely_summable by Def1;
hence thesis by A17,A18,Def2,COMSEQ_3:def 9;
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(|.seq_id(
vseq.m-vseq.n).|).i ) holds rseq is convergent & lim rseq = Partial_Sums(|.(
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(|.seq_id(vseq.m-vseq.n).|).$1 holds
rseq is convergent & lim rseq = Partial_Sums(|.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 Th5;
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(|.seq_id(vseq.m-vseq.n).|).i ) holds rseq is convergent &
lim rseq = Partial_Sums(|.((seq_id tseq-seq_id(vseq.n))).|).i;
thus for rseq be Real_Sequence st ( for m be Nat holds rseq
.m = Partial_Sums(|.seq_id(vseq.m-vseq.n).|).(i+1) ) holds rseq is convergent &
lim rseq =Partial_Sums(|.((seq_id tseq-seq_id(vseq.n))).|).(i+1)
proof
deffunc F(Nat) = Partial_Sums(|.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 Complex_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(|.
seq_id(vseq.m-vseq.n).|).(i+1);
A27: now
let m be Nat;
thus rseq.m = Partial_Sums(|.(seq_id(vseq.m-vseq.n)).|).(i+1) by
A26
.=|.(seq_id(vseq.m-vseq.n)).| .(i+1) +Partial_Sums(|.seq_id(
vseq.m-vseq.n).|).i by SERIES_1:def 1
.=|.seq_id(vseq.m)-seq_id(vseq.n).| .(i+1) +Partial_Sums(|.
seq_id(vseq.m-vseq.n).|).i by A20
.=|.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
VALUED_1:18
.=|.((seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1)).| + rseqb
.m by VALUED_1:1
.=|.((seq_id(vseq.m)).(i+1)+-(seq_id(vseq.n)).(i+1)).| + rseqb
.m by VALUED_1:8
.= |.((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
VALUED_1:8
.= |.((tseq-(seq_id(vseq.n))).(i+1) ).| + lim rseqb by VALUED_1:1
.= |.(tseq-(seq_id(vseq.n))).| .(i+1) + lim rseqb by VALUED_1:18
.= |.(tseq-(seq_id(vseq.n))).| .(i+1) + Partial_Sums(|.((seq_id
tseq -seq_id(vseq.n))).|).i by A21,A22
.= Partial_Sums (|.((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(|.seq_id(
vseq.m-vseq.n).|).0;
thus rseq is convergent & lim rseq = Partial_Sums(|.seq_id tseq-seq_id
(vseq.n).|).0
proof
consider rseq0 be Complex_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(|.seq_id(vseq.m-vseq.n).|).0 by A30
.=(|.seq_id(vseq.m-vseq.n).|).0 by SERIES_1:def 1
.=(|.seq_id(vseq.m)-seq_id(vseq.n).|).0 by A20
.=|.((seq_id(vseq.m)+-seq_id(vseq.n)).0).| by VALUED_1:18
.=|.((seq_id(vseq.m)).0+(-seq_id(vseq.n)).0).| by VALUED_1:1
.=|.((seq_id(vseq.m)).0+-(seq_id(vseq.n)).0).| by VALUED_1:8
.=|.((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 VALUED_1:8
.= |.((tseq-(seq_id((vseq.n)))).0).| by VALUED_1:1
.= |.(seq_id tseq-(seq_id(vseq.n))).| .0 by VALUED_1:18
.=Partial_Sums(|.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 |.(seq_id tseq-seq_id(vseq.n)
).| is summable & Sum |.(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(|.((seq_id
tseq -seq_id(vseq.n))).|).i <=e
proof
let i be Nat such that
0 <=i;
deffunc F(Nat)= Partial_Sums(|.(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(|.(seq_id(vseq.m-vseq.n)).|).i by A38;
assume
A41: m >= k;
then |.(seq_id((vseq.m) - (vseq.n))).| is summable & for i be
Nat holds 0 <= |.seq_id(vseq.m-vseq.n).| .i by A16,A36;
then
A42: Partial_Sums(|.(seq_id((vseq.m) - (vseq.n))).|).i <=Sum(|.(
seq_id((vseq.m) - (vseq.n))).|) by RSSPACE2:3;
Sum(|.(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(|.(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(|.((seq_id tseq -seq_id(vseq.n))).|).i <=e by A37,NAT_1:2;
hence Partial_Sums(|.((seq_id tseq -seq_id(vseq.n))).|).i < e1 by A14,
XXREAL_0:2;
end;
then
A43: Partial_Sums(|.((seq_id tseq -seq_id(vseq.n))).|) is bounded_above
by SEQ_2:def 3;
A44: for i be Nat holds 0 <= |.(seq_id tseq-seq_id(vseq.n)).| .i
proof
let i be Nat;
|.(seq_id tseq -seq_id(vseq.n)).| .i =|.((seq_id tseq -seq_id(
vseq.n)).i).| by VALUED_1:18;
hence thesis by COMPLEX1:46;
end;
then |.((seq_id tseq-seq_id(vseq.n))).| is summable by A43,SERIES_1:17;
then Partial_Sums(|.((seq_id tseq -seq_id(vseq.n))).|) is convergent by
SERIES_1:def 2;
then Sum(|.((seq_id tseq -seq_id(vseq.n))).|) = lim Partial_Sums(|.((
seq_id tseq - seq_id(vseq.n))).|) & lim Partial_Sums(|.((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;
|.seq_id tseq.| is summable
proof
set d=|.seq_id tseq.|;
A45: for i be Nat holds 0 <= |.(seq_id tseq).| .i
proof
let i be Nat;
|.(seq_id tseq).| .i = |.((seq_id tseq).i).| by VALUED_1:18;
hence thesis by COMPLEX1:46;
end;
reconsider jj=1 as Real;
consider m be Nat such that
A46: for n be Nat st n >= m holds |.((seq_id tseq -seq_id(
vseq.n))).| is summable & Sum(|.((seq_id tseq -seq_id(vseq.n))).|) < 1 by A12;
set b=|.seq_id(vseq.m).|;
set a=|.(seq_id tseq -seq_id(vseq.m)).|;
seq_id(vseq.m) is absolutely_summable by Def1;
then
A47: |.(seq_id(vseq.m)).| is summable by COMSEQ_3:def 9;
A48: for i be Nat holds d.i <= (a+b).i
proof
let i be Nat;
A49: i in NAT by ORDINAL1:def 12;
A50: b.i=|.((seq_id(vseq.m)).i).| & d.i=|.((seq_id tseq).i).| by VALUED_1:18;
a.i = |.((seq_id tseq+-seq_id(vseq.m)).i).| by VALUED_1:18
.= |.((seq_id tseq).i+(-seq_id(vseq.m)).i).| by VALUED_1:1,A49
.= |.((seq_id tseq).i+(-(seq_id(vseq.m)).i)).| by VALUED_1:8
.=|.((seq_id tseq).i-(seq_id(vseq.m)).i).|;
then d.i-b.i <= a.i by A50,COMPLEX1:59;
then d.i-b.i+b.i<= a.i + b.i by XREAL_1:6;
hence thesis by SEQ_1:7;
end;
|.((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
A51: seq_id tseq is absolutely_summable by COMSEQ_3:def 9;
A52: tseq in the_set_of_ComplexSequences by FUNCT_2:8;
then reconsider tv=tseq as Point of Complex_l1_Space by A51,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
A53: for n be Nat st n >= m holds |.(seq_id tseq-seq_id(
vseq.n)).| is summable & Sum(|.(seq_id tseq-seq_id(vseq.n)).|) < e by A12;
now
reconsider u=tseq as VECTOR of Complex_l1_Space by A51,A52,Def1;
let n be Nat;
assume n >= m;
then
A54: Sum |.(seq_id tseq-seq_id(vseq.n)).| < e by A53;
reconsider v=vseq.n as VECTOR of Complex_l1_Space;
seq_id(u-v) = u-v by Th5;
then Sum |. seq_id(u-v).| = Sum |.(seq_id tseq-seq_id(vseq.n)).| by Th5;
then
A55: (the normF of Complex_l1_Space).(u-v) < e by A54,Def2;
||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33
.=||.tv-(vseq.n).|| by CLVECT_1:103;
hence ||.(vseq.n) - tv.|| < e by A55;
end;
hence thesis;
end;
hence thesis by CLVECT_1:def 15;
end;