let p be Real; :: thesis: ( 1 <= p implies for lp being RealNormSpace st lp = NORMSTR(# ,,,,() #) 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(# ,,,,() #) holds
for vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent

A2: 1 / p > 0 by ;
let lp be RealNormSpace; :: thesis: ( lp = NORMSTR(# ,,,,() #) implies for vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent )

assume A3: lp = NORMSTR(# ,,,,() #) ; :: 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 ;
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 ;
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 ;
then (Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p) < e by ;
then A12: ((Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) to_power p < e to_power p by ;
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 ; :: 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 ;
hence a to_power (b * c) = 0 by ; :: 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 ;
hence (a to_power b) to_power c = 0 by ; :: 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 ; :: 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
.= |.((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 ;
((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
.= Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p) by ;
then A34: ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i < e to_power p by ;
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 ;
(e to_power p) to_power (1 / p) = e to_power ((1 / p) * p) by
.= e to_power 1 by
.= 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 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 ;
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 ;
A51: rseqb is convergent by ;
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
.= (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 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 ;
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 ;
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 ;
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 ;
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 ; :: 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 ;
A68: e1 to_power p = (e2 / 2) to_power ((1 / p) * p) by
.= (e2 / 2) to_power 1 by
.= 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
.= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by ;
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 ;
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 ;
(seq_id ((vseq . m) - (vseq . n))) rto_power p is summable by ;
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 ;
Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 by ;
hence rseq . m <= e2 / 2 by ; :: thesis: verum
end;
A78: lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i by ;
rseq is convergent by ;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 by ; :: 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 ;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2 by ; :: 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 ; :: thesis: verum
end;
then ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable by ;
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 ;
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 ; :: 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 ;
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 ;
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 ; :: thesis: verum
end;
then A90: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) >= 0 by ;
A91: (e to_power p) to_power (1 / p) = e to_power (p * (1 / p)) by
.= e to_power 1 by
.= 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
.= ||.(- ((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