let R be real-valued FinSequence; :: thesis: for n being Nat holds (MIM R) /^ n = MIM (R /^ n)
let n be Nat; :: thesis: (MIM R) /^ n = MIM (R /^ n)
set mf = MIM R;
set fn = R /^ n;
set mn = MIM (R /^ n);
A1: len (MIM R) = len R by Def2;
A2: len (MIM (R /^ n)) = len (R /^ n) by Def2;

now :: thesis: ( ( len R < n & (MIM R) /^ n = MIM (R /^ n) ) or ( n <= len R & (MIM R) /^ n = MIM (R /^ n) ) )

per cases ( len R < n or n <= len R ) ;

case A3: len R < n ; :: thesis: (MIM R) /^ n = MIM (R /^ n)

then (MIM R) /^ n = <*> REAL by A1, Def1;
hence (MIM R) /^ n = MIM (R /^ n) by A3, Def1, Th12; :: thesis: verum

end;

case A4: n <= len R ; :: thesis: (MIM R) /^ n = MIM (R /^ n)

then A5: len ((MIM R) /^ n) = (len R) - n by A1, Def1;
A6: len (MIM (R /^ n)) = len (R /^ n) by Def2;
then A7: dom (MIM (R /^ n)) = Seg (len (R /^ n)) by FINSEQ_1:def 3;
A8: Seg (len ((MIM R) /^ n)) = dom ((MIM R) /^ n) by FINSEQ_1:def 3;
A9: len (R /^ n) = (len R) - n by A4, Def1;
A10: Seg (len (R /^ n)) = dom (R /^ n) by FINSEQ_1:def 3;

now :: thesis: for m being Nat st m in dom (MIM (R /^ n)) holds
((MIM R) /^ n) . m = (MIM (R /^ n)) . m

let m be Nat; :: thesis: ( m in dom (MIM (R /^ n)) implies ((MIM R) /^ n) . m = (MIM (R /^ n)) . m )
set r1 = R . (m + n);
assume A11: m in dom (MIM (R /^ n)) ; :: thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m
then A12: 1 <= m by A7, FINSEQ_1:1;
A13: m <= len (R /^ n) by A7, A11, FINSEQ_1:1;
A14: (R /^ n) . m = R . (m + n) by A4, A10, A7, A11, Def1;
m <= m + n by NAT_1:11;
then A15: 1 <= m + n by A12, XXREAL_0:2;

now :: thesis: ( ( m = len (R /^ n) & ((MIM R) /^ n) . m = (MIM (R /^ n)) . m ) or ( m <> len (R /^ n) & ((MIM R) /^ n) . m = (MIM (R /^ n)) . m ) )

per cases ( m = len (R /^ n) or m <> len (R /^ n) ) ;

case A16: m = len (R /^ n) ; :: thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m

thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A1, A4, A5, A9, A8, A7, A11, Def1
.= R . (m + n) by A1, A9, A16, Def2
.= (MIM (R /^ n)) . m by A6, A14, A16, Def2 ; :: thesis: verum

end;

case m <> len (R /^ n) ; :: thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m

then m < len (R /^ n) by A13, XXREAL_0:1;
then A17: m + 1 <= len (R /^ n) by NAT_1:13;
then A18: m <= (len (R /^ n)) - 1 by XREAL_1:19;
set r2 = R . ((m + 1) + n);
A19: (m + 1) + n = (m + n) + 1 ;
1 <= m + 1 by NAT_1:11;
then m + 1 in dom (R /^ n) by A17, FINSEQ_3:25;
then A20: (R /^ n) . (m + 1) = R . ((m + 1) + n) by A4, Def1;
(m + 1) + n <= len R by A9, A17, XREAL_1:19;
then A21: m + n <= (len R) - 1 by A19, XREAL_1:19;
thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A1, A4, A5, A9, A8, A7, A11, Def1
.= (R . (m + n)) - (R . ((m + 1) + n)) by A1, A15, A19, A21, Def2
.= (MIM (R /^ n)) . m by A2, A12, A14, A18, A20, Def2 ; :: thesis: verum

end;

end;

end;

hence ((MIM R) /^ n) . m = (MIM (R /^ n)) . m ; :: thesis: verum

end;

hence (MIM R) /^ n = MIM (R /^ n) by A5, A9, A6, FINSEQ_2:9; :: thesis: verum

end;

end;

end;

hence (MIM R) /^ n = MIM (R /^ n) ; :: thesis: verum