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;

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) ) )end;

hence
(MIM R) /^ n = MIM (R /^ n)
; :: thesis: verumper cases
( len R < n or n <= len R )
;

end;

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;hence (MIM R) /^ n = MIM (R /^ n) by A3, Def1, Th12; :: thesis: verum

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;

end;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

hence
(MIM R) /^ n = MIM (R /^ n)
by A5, A9, A6, FINSEQ_2:9; :: thesis: verum((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;

end;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 ) )end;

hence
((MIM R) /^ n) . m = (MIM (R /^ n)) . m
; :: thesis: verumper cases
( m = len (R /^ n) or m <> len (R /^ n) )
;

end;

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;.= R . (m + n) by A1, A9, A16, Def2

.= (MIM (R /^ n)) . m by A6, A14, A16, Def2 ; :: thesis: verum

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;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