theorem Th10: :: RFINSEQ:10

for R being real-valued FinSequence
for n being Nat st len R = n + 2 holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*(R . (n + 1))*>