theorem Th16: :: RFINSEQ:16

for R being real-valued FinSequence st len R <> 0 holds
Sum (MIM R) = R . 1