let R be FinSequence of REAL ; :: thesis: for n being Element of NAT holds (MIM R) /^ n = MIM (R /^ n)
let n be Element of 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 & len (MIM (R /^ n)) = len (R /^ n) ) by Def3;

now

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

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

then ( (MIM R) /^ n = <*> REAL & R /^ n = <*> REAL ) by A1, Def2;
hence (MIM R) /^ n = MIM (R /^ n) by Th25; :: thesis: verum

end;

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

then A3: ( len ((MIM R) /^ n) = (len R) - n & ( for m being Element of NAT st m in dom ((MIM R) /^ n) holds
((MIM R) /^ n) . m = (MIM R) . (m + n) ) ) by A1, Def2;
A4: ( len (R /^ n) = (len R) - n & ( for m being Element of NAT st m in dom (R /^ n) holds
(R /^ n) . m = R . (m + n) ) ) by A2, Def2;
A5: len (MIM (R /^ n)) = len (R /^ n) by Def3;
A6: ( Seg (len (R /^ n)) = dom (R /^ n) & Seg (len ((MIM R) /^ n)) = dom ((MIM R) /^ n) ) by FINSEQ_1:def 3;
X: dom (MIM (R /^ n)) = Seg (len (R /^ n)) by A5, FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom (MIM (R /^ n)) implies ((MIM R) /^ n) . m = (MIM (R /^ n)) . m )
assume A7: m in dom (MIM (R /^ n)) ; :: thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m
then A8: ( 1 <= m & m <= len (R /^ n) ) by X, FINSEQ_1:3;
m <= m + n by NAT_1:11;
then A9: ( 1 <= m + n & m + n <= len R ) by A4, A8, XREAL_1:21, XXREAL_0:2;
set r1 = R . (m + n);
A10: (R /^ n) . m = R . (m + n) by A2, A6, A7, Def2, X;

now

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

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

thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A3, A4, A6, A7, X
.= R . (m + n) by A1, A4, A11, Def3
.= (MIM (R /^ n)) . m by A5, A10, A11, Def3 ; :: thesis: verum

end;

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

then m < len (R /^ n) by A8, XXREAL_0:1;
then A12: m + 1 <= len (R /^ n) by NAT_1:13;
then A13: ( (m + 1) + n <= len R & m <= m + 1 & m + 1 <= (m + 1) + n ) by A4, NAT_1:11, XREAL_1:21;
set r2 = R . ((m + 1) + n);
A14: (m + 1) + n = (m + n) + 1 ;
then A15: ( m + n <= (len R) - 1 & m <= (len (R /^ n)) - 1 ) by A12, A13, XREAL_1:21;
1 <= m + 1 by NAT_1:11;
then m + 1 in dom (R /^ n) by A12, FINSEQ_3:27;
then A16: (R /^ n) . (m + 1) = R . ((m + 1) + n) by A2, Def2;
thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A3, A4, A6, A7, X
.= (R . (m + n)) - (R . ((m + 1) + n)) by A1, A9, A14, A15, Def3
.= (MIM (R /^ n)) . m by A1, A8, A10, A15, A16, Def3 ; :: 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 A3, A4, A5, FINSEQ_2:10; :: thesis: verum

end;

end;

end;

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