for m being Nat
for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )