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:141;
A3: p * (1 / p) = (p * 1) / p by XCMPLX_1:75
.= 1 by A1, XCMPLX_1:60 ;
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 A4: 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 A5: vseq is CCauchy ; :: thesis: vseq is convergent
defpred S₁[ 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 ) );
A6: for x being set st x in NAT holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume A7: x in NAT ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
reconsider i = x as Element of NAT by A7;
deffunc H₁( Element of NAT ) -> Element of REAL = (seq_id (vseq . $1)) . i;
consider rseqi being Real_Sequence such that
A8: for n being Element of NAT holds rseqi . n = H₁(n) from SEQ_1:sch 1();
A9: rseqi is convergent

proof

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 A10: 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
A11: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A5, A10, RSSPACE3:10;
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 A12: k <= m ; :: thesis: abs ((rseqi . m) - (rseqi . k)) < e
A13: ||.((vseq . m) - (vseq . k)).|| = the norm of lp . ((vseq . m) - (vseq . k)) by NORMSP_1:def 1
.= (Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p) by A4, Def3 ;
then (Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p) < e by A11, A12;
then A14: ((Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) to_power p < e to_power p by A1, A13, Th1, NORMSP_1:8;
A15: (seq_id ((vseq . m) - (vseq . k))) rto_power p is summable by A1, A4, Th10;

A16: 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:132; :: thesis: verum

end;

then 0 <= Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p) by A15, SERIES_1:21;
then A17: ((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, HOLDER_1:2
.= Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p) by A3, POWER:30 ;
A18: (e to_power p) to_power (1 / p) = e to_power ((1 / p) * p) by A10, POWER:38
.= e to_power 1 by A1, XCMPLX_1:107
.= e by POWER:30 ;
A19: ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i <= Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p) by A15, A16, RSSPACE2:4;

A20: now

let a, b, c be Real; :: thesis: ( a = 0 & b > 0 & c > 0 implies (a to_power b) to_power c = 0 )
assume A21: ( a = 0 & b > 0 & c > 0 ) ; :: thesis: (a to_power b) to_power c = 0
a to_power b = 0 by A21, 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 * c) = 0 )
assume A23: ( a = 0 & b > 0 & c > 0 ) ; :: thesis: a to_power (b * c) = 0
b * c > 0 by A23, XREAL_1:131;
hence a to_power (b * c) = 0 by A23, POWER:def 2; :: thesis: verum

end;

A24: 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 A25: ( a = 0 & b > 0 & 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 A20, A25
.= a to_power (b * c) by A22, 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 A27: ( a >= 0 & b > 0 & c > 0 ) ; :: thesis: (a to_power b) to_power c = a to_power (b * c)
( ( a > 0 or a = 0 ) & b > 0 & c > 0 ) by A27;
hence (a to_power b) to_power c = a to_power (b * c) by A24, POWER:38; :: 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 A28: (((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, A3, A26, COMPLEX1:132
.= abs ((seq_id ((vseq . m) - (vseq . k))) . i) by POWER:30 ;
A29: ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i < e to_power p by A14, A17, A19, XXREAL_0:2;
A30: ( rseqi . m = (seq_id (vseq . m)) . i & rseqi . k = (seq_id (vseq . k)) . i ) by A8;
reconsider vsem = vseq . m, vsek = vseq . k as VECTOR of lp ;
vsem - vsek = (seq_id vsem) - (seq_id vsek) by A1, A4, Th10;
then abs ((seq_id ((vseq . m) - (vseq . k))) . i) = abs (((seq_id (vseq . m)) + (- (seq_id (vseq . k)))) . i) by RSSPACE:3
.= abs (((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i)) by SEQ_1:11
.= abs (((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i))) by SEQ_1:14
.= abs ((rseqi . m) - (rseqi . k)) by A30 ;
hence abs ((rseqi . m) - (rseqi . k)) < e by A2, A16, A18, A28, A29, 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;

hence rseqi is convergent by SEQ_4:58; :: thesis: verum

end;

take y = lim rseqi; :: thesis: ( y in REAL & S₁[x,y] )
thus ( y in REAL & S₁[x,y] ) by A8, A9; :: thesis: verum

end;

consider f being Function of NAT ,REAL such that
A31: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A6);
reconsider tseq = f as Real_Sequence ;

A32: 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 A31;
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;

A33: 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

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 A34: 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;
A35: e2 / 2 > 0 by A34, XREAL_1:217;
A36: e2 > e2 / 2 by A34, XREAL_1:218;
set e1 = (e2 / 2) to_power (1 / p);
(e2 / 2) to_power (1 / p) > 0 by A35, POWER:39;
then consider k being Element of NAT such that
A37: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < (e2 / 2) to_power (1 / p) by A5, RSSPACE3:10;
A38: 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 A39: ( n >= k & 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 ) )
A40: 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:132; :: thesis: verum

end;

||.((vseq . m) - (vseq . n)).|| < (e2 / 2) to_power (1 / p) by A37, A39;
then the norm of lp . ((vseq . m) - (vseq . n)) < (e2 / 2) to_power (1 / p) by NORMSP_1:def 1;
then A41: (Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p) < (e2 / 2) to_power (1 / p) by A4, Def3;
(seq_id ((vseq . m) - (vseq . n))) rto_power p is summable by A1, A4, Th10;
then A42: 0 <= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by A40, SERIES_1:21;
then A43: ((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, HOLDER_1:2
.= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by A3, POWER:30 ;
A44: ((e2 / 2) to_power (1 / p)) to_power p = (e2 / 2) to_power ((1 / p) * p) by A35, POWER:38
.= (e2 / 2) to_power 1 by A1, XCMPLX_1:107
.= e2 / 2 by POWER:30 ;
(Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p) >= 0 by A2, A42, Lm1;
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, A4, A40, A41, A43, A44, Th1, Th10; :: thesis: verum

end;

A45: 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 )
A46: 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, A4, Th10;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:3; :: thesis: verum

end;

defpred S₂[ 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 );
A47: S₂[ 0 ]

proof

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 A48: 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
A49: ( ( for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 ) & rseq0 is convergent & tseq . 0 = lim rseq0 ) by A32;
A50: 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 A48
.= ((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 A46
.= (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:11
.= (abs (((seq_id (vseq . m)) . 0 ) + (- ((seq_id (vseq . n)) . 0 )))) to_power p by SEQ_1:14
.= (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 A49; :: thesis: verum

end;

then lim rseq = (abs ((lim rseq0) - ((seq_id (vseq . n)) . 0 ))) to_power p by A1, A49, Lm9
.= (abs ((tseq . 0 ) + (- ((seq_id (vseq . n)) . 0 )))) to_power p by A49
.= (abs ((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 ))) to_power p by SEQ_1:14
.= (abs ((tseq - (seq_id (vseq . n))) . 0 )) to_power p by SEQ_1:11
.= (abs (((seq_id tseq) + (- (seq_id (vseq . n)))) . 0 )) to_power p by RSSPACE:3
.= (((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, A49, A50, Lm9; :: thesis: verum

end;

end;

hence S₂[ 0 ] ; :: thesis: verum

end;

A51: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

proof

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 A52: 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

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 A53: 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) )
deffunc H₁( 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
A54: for m being Element of NAT holds rseqb . m = H₁(m) from SEQ_1:sch 1();
A55: ( rseqb is convergent & lim rseqb = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i ) by A52, A54;
consider rseq0 being Real_Sequence such that
A56: ( ( for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) ) & rseq0 is convergent & tseq . (i + 1) = lim rseq0 ) by A32;

A57: 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 A53
.= (((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 A46
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) rto_power p) . (i + 1)) + (rseqb . m) by A54
.= ((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:11
.= ((abs (((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) to_power p) + (rseqb . m) by SEQ_1:14
.= ((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 A56 ; :: thesis: verum

end;

then lim rseq = ((abs ((lim rseq0) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (lim rseqb) by A1, A55, A56, Lm10
.= ((abs ((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) to_power p) + (lim rseqb) by A56
.= ((abs ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) to_power p) + (lim rseqb) by SEQ_1:14
.= ((abs ((tseq - (seq_id (vseq . n))) . (i + 1))) to_power p) + (lim rseqb) by SEQ_1:11
.= (((tseq - (seq_id (vseq . n))) rto_power p) . (i + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i) by A55, 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:3
.= (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, A55, A56, A57, Lm10; :: thesis: verum

end;

end;

hence for i being Element of NAT st S₂[i] holds
S₂[i + 1] ; :: thesis: verum

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A47, 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;

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 A58: 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 )
A59: 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 H₁( 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
A60: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
A61: rseq is convergent by A45, A60;
A62: lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i by A45, A60;
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 )
assume m >= k ; :: thesis: rseq . m <= e2 / 2
then A63: ( (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 A38, A58;
then A64: (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i <= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by RSSPACE2:4;
rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i by A60;
hence rseq . m <= e2 / 2 by A63, A64, XXREAL_0:2; :: thesis: verum

end;

hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 by A61, A62, RSSPACE2:6; :: thesis: verum

end;

A65: 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:132; :: thesis: verum

end;

A66: Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) is bounded_above

proof

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
A67: e2 > e2 / 2 by XREAL_1:31;
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 A59, NAT_1:2;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2 by A67, XXREAL_0:2; :: thesis: verum

end;

hence Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) is bounded_above by SEQ_2:def 3; :: thesis: verum

end;

A68: 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;
((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable by A65, A66, SERIES_1:20;
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 A59, RSSPACE2:6;
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 A36, A65, A66, A68, SERIES_1:20, 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
A69: 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 A33;
A70: ((seq_id tseq) - (seq_id (vseq . m))) rto_power p is summable by A69;
A71: (seq_id (vseq . m)) rto_power p is summable by A1, A4, Def2;
set a = (seq_id tseq) - (seq_id (vseq . m));
set b = seq_id (vseq . m);
set d = seq_id tseq;
((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:20
.= ((seq_id tseq) + (seq_id (vseq . m))) - (seq_id (vseq . m))
.= seq_id tseq by Lm11 ;
hence (seq_id tseq) rto_power p is summable by A1, A70, A71, Lm12; :: thesis: verum

end;

then reconsider tv = tseq as Point of lp by A1, A4, 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 A72: 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;
e to_power p > 0 by A72, POWER:39;
then consider m being Element of NAT such that
A73: 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 A33;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A74: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
A75: 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:132; :: thesis: verum

end;

((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable by A73, A74;
then A76: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) >= 0 by A75, SERIES_1:21;
A77: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e to_power p by A73, A74;
A78: (e to_power p) to_power (1 / p) = e to_power (p * (1 / p)) by A72, POWER:38
.= e to_power 1 by A1, XCMPLX_1:107
.= e by POWER:30 ;
(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:3
.= (Sum ((seq_id (tv - (vseq . n))) rto_power p)) to_power (1 / p) by A1, A4, Th10
.= the norm of lp . (tv - (vseq . n)) by A4, Def3
.= ||.(tv + (- (vseq . n))).|| by NORMSP_1:def 1
.= ||.(- ((vseq . n) - tv)).|| by RLVECT_1:47
.= ||.((vseq . n) - tv).|| by NORMSP_1:6 ;
hence ||.((vseq . n) - tv).|| < e by A2, A76, A77, A78, 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 9; :: thesis: verum