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