for p being FinSequence of REAL
for i being Element of NAT st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))