let R be FinSequence of REAL ; for n being Nat holds (MIM R) /^ n = MIM (R /^ n)
let n be Nat; (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 ( ( 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 A4:
n <= len R
;
(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 for m being Nat st m in dom (MIM (R /^ n)) holds
((MIM R) /^ n) . m = (MIM (R /^ n)) . mlet m be
Nat;
( 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))
;
((MIM R) /^ n) . m = (MIM (R /^ n)) . mthen 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 ( ( 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)
;
((MIM R) /^ n) . m = (MIM (R /^ n)) . mthus ((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
;
verum end; case
m <> len (R /^ n)
;
((MIM R) /^ n) . m = (MIM (R /^ n)) . mthen
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
;
verum end; hence
((MIM R) /^ n) . m = (MIM (R /^ n)) . m
;
verum end; hence
(MIM R) /^ n = MIM (R /^ n)
by A5, A9, A6, FINSEQ_2:9;
verum end;
hence
(MIM R) /^ n = MIM (R /^ n)
; verum