theorem Th10: :: RFINSEQ:10

for R being FinSequence of REAL
for r being Real
for n being Nat st len R = n + 2 & R . (n + 1) = r holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>