let R be FinSequence of REAL ; :: 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 ;
hence (MIM R) /^ n = MIM (R /^ n) by ; :: 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 ;
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 ;
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 ;
A13: m <= len (R /^ n) by ;
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 ;
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 ;
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 ;
then A20: (R /^ n) . (m + 1) = R . ((m + 1) + n) by ;
(m + 1) + n <= len R by ;
then A21: m + n <= (len R) - 1 by ;
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 ; :: thesis: verum
end;
end;
end;
hence (MIM R) /^ n = MIM (R /^ n) ; :: thesis: verum