theorem Th16: :: RFINSEQ:16

for R being FinSequence of REAL st len R <> 0 holds
Sum (MIM R) = R . 1