defpred S₁[ Nat] means for seq being Real_Sequence
for sq being FinSequence of REAL st len sq = $1 & ( for k being Nat st k < $1 holds
seq . k = sq . (k + 1) ) & ( for k being Nat st k >= $1 holds
seq . k = 0 ) holds
( seq is summable & Sum seq = Sum sq );

let n be Nat; :: thesis:
assume A1: for seq being Real_Sequence
for sq being FinSequence of REAL st len sq = n & ( for k being Nat st k < n holds
seq . k = sq . (k + 1) ) & ( for k being Nat st k >= n holds
seq . k = 0 ) holds
( seq is summable & Sum seq = Sum sq ) ; :: thesis:
let seq be Real_Sequence; :: thesis:
let sq be FinSequence of REAL ; :: thesis:
assume that
A2: len sq = n + 1 and
A3: for k being Nat st k < n + 1 holds
seq . k = sq . (k + 1) and
A4: for k being Nat st k >= n + 1 holds
seq . k = 0 ; :: thesis:

let k be Nat; :: thesis:
A6: k + 1 >= 0 + 1 by XREAL_1:6;
assume k < n ; :: thesis:
then A7: k + 1 < n + 1 by XREAL_1:6;
thus (seq ^\ 1) . k = seq . (k + 1) by NAT_1:def 3
.= sq . ((k + 1) + 1) by A3, A7
.= (sq /^ 1) . (k + 1) by A2, A7, A6, Th16 ; :: thesis:

end;

A8: now :: thesis:

let k be Nat; :: thesis:
assume k >= n ; :: thesis:
then A9: k + 1 >= n + 1 by XREAL_1:6;
thus (seq ^\ 1) . k = seq . (k + 1) by NAT_1:def 3
.= 0 by A4, A9 ; :: thesis:

end;

n + 1 >= 0 + 1 by XREAL_1:6;
then A10: len (sq /^ 1) = (len sq) - 1 by A2, RFINSEQ:def 1
.= n by A2 ;
then A11: Sum (seq ^\ 1) = Sum (sq /^ 1) by A1, A5, A8;
A12: seq ^\ 1 is summable by A1, A10, A5, A8;
hence seq is summable by Th15; :: thesis:
thus Sum seq = (seq . 0) + (Sum (seq ^\ 1)) by A12, Th15
.= (sq . (0 + 1)) + (Sum (seq ^\ 1)) by A3
.= Sum sq by A2, A11, Th17 ; :: thesis:

end;

then A13: for k being Nat st S₁[k] holds
S₁[k + 1] ;

now :: thesis:

let seq be Real_Sequence; :: thesis:
let sq be FinSequence of REAL ; :: thesis:
assume that
A14: len sq = 0 and
for k being Nat st k < 0 holds
seq . k = sq . (k + 1) and
A15: for k being Nat st k >= 0 holds
seq . k = 0 ; :: thesis:
sq is Element of 0 -tuples_on REAL by A14, FINSEQ_2:92;
then A16: Sum sq = 0 by RVSUM_1:79;
defpred S₂[ Nat] means (Partial_Sums seq) . $1 = 0 ;

A17: now :: thesis:

let k be Nat; :: thesis:
A18: (Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SERIES_1:def 1;
assume S₂[k] ; :: thesis:
hence S₂[k + 1] by A15, A18; :: thesis:

end;

seq . 0 = 0 by A15;
then A19: S₂[ 0 ] by SERIES_1:def 1;
A20: for k being Nat holds S₂[k] from NAT_1:sch 2(A19, A17);
then Partial_Sums seq is convergent by Th9;
hence seq is summable by SERIES_1:def 2; :: thesis:
lim (Partial_Sums seq) = 0 by A20, Th9;
hence Sum seq = Sum sq by A16, SERIES_1:def 3; :: thesis:

end;

then A21: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A21, A13); :: thesis: