let p be Real; :: thesis: ( 1 <= p implies for lp being 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 being sequence of lp st vseq is CCauchy holds
vseq is convergent )
assume A1: 1 <= p ; :: thesis: for lp being 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 being sequence of lp st vseq is CCauchy holds
vseq is convergent
A2: 1 / p > 0 by A1, XREAL_1:139;
let lp be RealNormSpace; :: thesis: ( 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) #) implies for vseq being sequence of lp st vseq is CCauchy holds
vseq is convergent )
assume 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) #) ; :: thesis: for vseq being sequence of lp st vseq is CCauchy holds
vseq is convergent
let vseq be sequence of lp; :: thesis: ( vseq is CCauchy implies vseq is convergent )
assume A4: vseq is CCauchy ; :: thesis: vseq is convergent
defpred S1[ set , set ] means ex i being Element of NAT st
( $1 = i & ex rseqi being Real_Sequence st
( ( for n being Element of 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 being set st x in NAT holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in REAL & S1[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H1( Element of NAT ) -> Element of REAL = (seq_id (vseq . $1)) . i;
consider rseqi being Real_Sequence such that
A7: for n being Element of NAT holds rseqi . n = H1(n) from SEQ_1:sch 1();
 take lim rseqi ; :: thesis: ( lim rseqi in REAL & S1[x, lim rseqi] )
now
let e1 be real number ; :: thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1 )
assume A8: e1 > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1
reconsider e = e1 as Real by XREAL_0:def 1;
thus ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1 :: thesis: verum
proof
consider k being Element of NAT such that
A9: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A4, A8, RSSPACE3:8;
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
proof
let m be Element of NAT ; :: thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume A10: k <= m ; :: thesis: abs ((rseqi . m) - (rseqi . k)) < e
A11: ||.((vseq . m) - (vseq . k)).|| = the normF of lp . ((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 Element of NAT ; :: thesis: ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i >= 0
((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i = (abs ((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; :: thesis: verum
end;
reconsider vsem = vseq . m, vsek = vseq . k as VECTOR of lp ;
A14: now
let a, b, c be Real; :: thesis: ( a = 0 & b > 0 & c > 0 implies a to_power (b * c) = 0 )
assume that
A15: a = 0 and
A16: b > 0 and
A17: c > 0 ; :: thesis: a to_power (b * c) = 0
b * c > 0 by A16, A17, XREAL_1:129;
hence a to_power (b * c) = 0 by A15, POWER:def 2; :: thesis: verum
end;
A18: now
let a, b, c be Real; :: thesis: ( a = 0 & b > 0 & c > 0 implies (a to_power b) to_power c = 0 )
assume that
A19: a = 0 and
A20: b > 0 and
A21: c > 0 ; :: thesis: (a to_power b) to_power 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; :: thesis: verum
end;
A22: now
let a, b, c be Real; :: thesis: ( a = 0 & b > 0 & c > 0 implies (a to_power b) to_power c = a to_power (b * c) )
assume that
A23: a = 0 and
A24: b > 0 and
A25: c > 0 ; :: thesis: (a to_power b) to_power c = a to_power (b * c)
thus (a to_power b) to_power c = 0 by A18, A23, A24, A25
.= a to_power (b * c) by A14, A23, A24, A25 ; :: thesis: verum
end;
A26: for a, b, c being 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; :: thesis: ( a >= 0 & b > 0 & c > 0 implies (a to_power b) to_power c = a to_power (b * c) )
assume that
A27: a >= 0 and
A28: b > 0 and
A29: c > 0 ; :: thesis: (a to_power b) to_power c = a to_power (b * c)
( a > 0 or a = 0 ) by A27;
hence (a to_power b) to_power c = a to_power (b * c) by A22, A28, A29, POWER:33; :: thesis: verum
end;
((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i = (abs ((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) = (abs ((seq_id ((vseq . m) - (vseq . k))) . i)) to_power 1 by A1, A2, A5, A26, COMPLEX1:46
.= abs ((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: abs ((seq_id ((vseq . m) - (vseq . k))) . i) = abs (((seq_id (vseq . m)) + (- (seq_id (vseq . k)))) . i) by RSSPACE:1
.= abs (((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i)) by SEQ_1:7
.= abs (((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i))) by SEQ_1:10
.= abs ((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 abs ((rseqi . m) - (rseqi . k)) < e by A2, A13, A30, A34, A36, Th1; :: thesis: verum
end;
hence ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1 ; :: thesis: verum
end;
end;
then rseqi is convergent by SEQ_4:41;
hence ( lim rseqi in REAL & S1[x, lim rseqi] ) by A7; :: thesis: verum
end;
consider f being Function of NAT,REAL such that
A37: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch 1(A6);
 reconsider tseq = f as Real_Sequence ;
A38: now
let i be Element of NAT ; :: thesis: ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
ex i0 being Element of NAT st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A37;
hence ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; :: thesis: verum
end;
A39: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of 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
A40: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 Element of NAT ; :: thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 )
defpred S2[ Element of NAT ] means for rseq being Real_Sequence st ( for m being Element of 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 );
A41: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
proof
let m, k be Element of NAT ; :: thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by A1, A3, Th10;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:1; :: thesis: verum
end;
now
let i be Element of NAT ; :: thesis: ( ( for rseq being Real_Sequence st ( for m being Element of 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 ) ) implies for rseq being Real_Sequence st ( for m being Element of 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) ) )
assume A42: for rseq being Real_Sequence st ( for m being Element of 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 ) ; :: thesis: for rseq being Real_Sequence st ( for m being Element of 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) )
thus for rseq being Real_Sequence st ( for m being Element of 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) ) :: thesis: verum
proof
deffunc H1( Element of NAT ) -> Element of REAL = (Partial_Sums ((seq_id ((vseq . $1) - (vseq . n))) rto_power p)) . i;
consider rseqb being Real_Sequence such that
A43: for m being Element of NAT holds rseqb . m = H1(m) from SEQ_1:sch 1();
 consider rseq0 being Real_Sequence such that
A44: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) and
A45: rseq0 is convergent and
A46: tseq . (i + 1) = lim rseq0 by A38;
let rseq be Real_Sequence; :: thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) ) implies ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) ) )
assume A47: for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) )
A48: now
let m be Element of NAT ; :: thesis: rseq . m = ((abs ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (rseqb . m)
thus rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) by A47
.= (((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 A41
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) rto_power p) . (i + 1)) + (rseqb . m) by A43
.= ((abs (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1))) to_power p) + (rseqb . m) by Def1
.= ((abs (((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) to_power p) + (rseqb . m) by SEQ_1:7
.= ((abs (((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) to_power p) + (rseqb . m) by SEQ_1:10
.= ((abs (((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (rseqb . m)
.= ((abs ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (rseqb . m) by A44 ; :: thesis: verum
end;
A49: lim rseqb = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i by A42, A43;
A50: rseqb is convergent by A42, A43;
then lim rseq = ((abs ((lim rseq0) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (lim rseqb) by A1, A45, A48, Lm10
.= ((abs ((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) to_power p) + (lim rseqb) by A46
.= ((abs ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) to_power p) + (lim rseqb) by SEQ_1:10
.= ((abs ((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 A49, Def1
.= ((((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . (i + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i) by RSSPACE:1
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) by SERIES_1:def 1 ;
hence ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) ) by A1, A50, A45, A48, Lm10; :: thesis: verum
end;
end;
then A51: for i being Element of NAT st S2[i] holds
S2[i + 1] ;
now
let rseq be Real_Sequence; :: thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 ) implies ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . 0 ) )
assume A52: for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (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 ) :: thesis: verum
proof
consider rseq0 being Real_Sequence such that
A53: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A54: rseq0 is convergent and
A55: tseq . 0 = lim rseq0 by A38;
A56: for m being Element of NAT holds rseq . m = (abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0))) to_power p
proof
let m be Element of NAT ; :: thesis: rseq . m = (abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0))) to_power p
rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 by A52
.= ((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 A41
.= (abs (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0)) to_power p by Def1
.= (abs (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0))) to_power p by SEQ_1:7
.= (abs (((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0)))) to_power p by SEQ_1:10
.= (abs (((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0))) to_power p ;
hence rseq . m = (abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0))) to_power p by A53; :: thesis: verum
end;
then lim rseq = (abs ((lim rseq0) - ((seq_id (vseq . n)) . 0))) to_power p by A1, A54, Lm9
.= (abs ((tseq . 0) + (- ((seq_id (vseq . n)) . 0)))) to_power p by A55
.= (abs ((tseq . 0) + ((- (seq_id (vseq . n))) . 0))) to_power p by SEQ_1:10
.= (abs ((tseq - (seq_id (vseq . n))) . 0)) to_power p by SEQ_1:7
.= (abs (((seq_id tseq) + (- (seq_id (vseq . n)))) . 0)) to_power p by RSSPACE:1
.= (((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 ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . 0 ) by A1, A54, A56, Lm9; :: thesis: verum
end;
end;
then A57: S2[ 0 ] ;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A57, A51);
 hence for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 ) ; :: thesis: verum
end;
let e2 be Real; :: thesis: ( e2 > 0 implies ex k being Element of NAT st
for n being Element of 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 ) )
assume A58: e2 > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of 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 )
set e = e2 / 2;
set e1 = (e2 / 2) to_power (1 / p);
e2 / 2 > 0 by A58, XREAL_1:215;
then (e2 / 2) to_power (1 / p) > 0 by POWER:34;
then consider k being Element of NAT such that
A59: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < (e2 / 2) to_power (1 / p) by A4, RSSPACE3:8;
A60: for m, n being Element of 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) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) )
proof
let m, n be Element of NAT ; :: thesis: ( n >= k & m >= k implies ( (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) ) )
assume that
A61: n >= k and
A62: m >= k ; :: thesis: ( (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) )
||.((vseq . m) - (vseq . n)).|| < (e2 / 2) to_power (1 / p) by A59, A61, A62;
then the normF of lp . ((vseq . m) - (vseq . n)) < (e2 / 2) to_power (1 / p) ;
then A63: (Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p) < (e2 / 2) to_power (1 / p) by A3, Def3;
A64: for i being Element of NAT holds ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i >= 0
proof
let i be Element of NAT ; :: thesis: ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i >= 0
((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i = (abs ((seq_id ((vseq . m) - (vseq . n))) . i)) to_power p by Def1;
hence ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:46; :: thesis: verum
end;
A65: (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable by A1, A3, Th10;
then A66: (Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p) >= 0 by A2, A64, Lm1, SERIES_1:18;
A67: ((e2 / 2) to_power (1 / p)) to_power p = (e2 / 2) to_power ((1 / p) * p) by A58, POWER:33, XREAL_1:215
.= (e2 / 2) to_power 1 by A1, XCMPLX_1:106
.= e2 / 2 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, A64, A65, HOLDER_1:2, SERIES_1:18
.= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by A5, POWER:25 ;
hence ( (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) ) by A1, A3, A64, A63, A67, A66, Th1, Th10; :: thesis: verum
end;
A68: e2 > e2 / 2 by A58, XREAL_1:216;
for n being Element of 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 Element of NAT ; :: thesis: ( n >= k implies ( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 ) )
assume A69: n >= k ; :: thesis: ( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 )
A70: for i being Element of NAT st 0 <= i holds
(Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2
proof
let i be Element of NAT ; :: thesis: ( 0 <= i implies (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 )
assume 0 <= i ; :: thesis: (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2
deffunc H1( Element of NAT ) -> Element of REAL = (Partial_Sums ((seq_id ((vseq . $1) - (vseq . n))) rto_power p)) . i;
consider rseq being Real_Sequence such that
A71: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch 1();
 A72: for m being Element of NAT st m >= k holds
rseq . m <= e2 / 2
proof
let m be Element of NAT ; :: thesis: ( m >= k implies rseq . m <= e2 / 2 )
A73: rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i by A71;
assume A74: m >= k ; :: thesis: rseq . m <= e2 / 2
then A75: for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i by A60, A69;
(seq_id ((vseq . m) - (vseq . n))) rto_power p is summable by A60, A69, A74;
then A76: (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i <= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by A75, RSSPACE2:3;
Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 by A60, A69, A74;
hence rseq . m <= e2 / 2 by A76, A73, XXREAL_0:2; :: thesis: verum
end;
A77: lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i by A40, A71;
rseq is convergent by A40, A71;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 by A77, A72, RSSPACE2:5; :: thesis: verum
end;
now
take e2 = (e2 / 2) + 1; :: thesis: for i being Element of NAT holds (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2
A78: e2 > e2 / 2 by XREAL_1:29;
let i be Element of NAT ; :: thesis: (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2
(Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 by A70, NAT_1:2;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2 by A78, XXREAL_0:2; :: thesis: verum
end;
then A79: Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) is bounded_above by SEQ_2:def 3;
A80: 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;
A81: for i being Element of NAT holds 0 <= (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i
proof
let i be Element of NAT ; :: thesis: 0 <= (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i
(((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i = (abs (((seq_id tseq) - (seq_id (vseq . n))) . i)) to_power p by Def1;
hence 0 <= (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i by A1, Lm1, COMPLEX1:46; :: thesis: verum
end;
then ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable by A79, 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)) <= e2 / 2 by A70, RSSPACE2:5;
hence ( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 ) by A68, A81, A79, A80, SERIES_1:17, XXREAL_0:2; :: thesis: verum
end;
hence ex k being Element of NAT st
for n being Element of 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 ) ; :: thesis: verum
end;
(seq_id tseq) rto_power p is summable
proof
consider m being Element of NAT such that
A82: for n being Element of 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 A39;
A83: ((seq_id tseq) - (seq_id (vseq . m))) rto_power p is summable by A82;
set d = seq_id tseq;
set b = seq_id (vseq . m);
set a = (seq_id tseq) - (seq_id (vseq . m));
A84: ((seq_id tseq) - (seq_id (vseq . m))) + (seq_id (vseq . m)) = ((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))
.= seq_id tseq by Lm11 ;
(seq_id (vseq . m)) rto_power p is summable by A1, A3, Def2;
hence (seq_id tseq) rto_power p is summable by A1, A83, A84, Lm12; :: thesis: verum
end;
then reconsider tv = tseq as Point of lp by A1, A3, Th10;
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; :: thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A85: e > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
set e1 = e to_power p;
consider m being Element of NAT such that
A86: for n being Element of 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) < e to_power p ) by A39, A85, POWER:34;
now
let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A87: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
A88: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e to_power p by A86, A87;
for i being Element of NAT holds (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i >= 0
proof
let i be Element of NAT ; :: thesis: (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i >= 0
(((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i = (abs (((seq_id tseq) - (seq_id (vseq . n))) . i)) to_power p by Def1;
hence (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:46; :: thesis: verum
end;
then A89: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) >= 0 by A86, A87, SERIES_1:18;
A90: (e to_power p) to_power (1 / p) = e to_power (p * (1 / p)) by A85, 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) by RSSPACE:1
.= (Sum ((seq_id (tv - (vseq . n))) rto_power p)) to_power (1 / p) by A1, A3, Th10
.= the normF of lp . (tv - (vseq . n)) by A3, Def3
.= ||.(tv + (- (vseq . n))).||
.= ||.(- ((vseq . n) - tv)).|| by RLVECT_1:33
.= ||.((vseq . n) - tv).|| by NORMSP_1:2 ;
hence ||.((vseq . n) - tv).|| < e by A2, A89, A88, A90, Th1; :: thesis: verum
end;
hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; :: thesis: verum
end;
hence vseq is convergent by NORMSP_1:def 6; :: thesis: verum