theorem :: RFINSEQ:15

for R being real-valued FinSequence
for n being Nat holds (MIM R) /^ n = MIM (R /^ n)