for n being Nat
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 )