for R being FinSequence of REAL
for n being Nat st n < len R holds
Sum (MIM (R /^ n)) = R . (n + 1)