for R being FinSequence of REAL
for n being Nat holds (MIM R) /^ n = MIM (R /^ n)