let R be FinSequence of REAL ; for n being Nat st len R = n + 2 holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*(R . (n + 1))*>
let n be Nat; ( len R = n + 2 implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*(R . (n + 1))*> )
assume A1:
len R = n + 2
; MIM (R | (n + 1)) = ((MIM R) | n) ^ <*(R . (n + 1))*>
set s = R . (n + 1);
set f1 = R | (n + 1);
set m1 = MIM (R | (n + 1));
set mf = MIM R;
set fn = (MIM R) | n;
A3:
0 + 1 <= n + 1
by NAT_1:13;
A4:
(n + 1) + 1 = n + (1 + 1)
;
then
n + 1 <= n + 2
by NAT_1:11;
then A5:
( Seg (len R) = dom R & n + 1 in Seg (n + 2) )
by A3, FINSEQ_1:def 3;
A6:
len (R | (n + 1)) = n + 1
by A1, A4, FINSEQ_1:59, NAT_1:11;
then A7:
len (MIM (R | (n + 1))) = n + 1
by Def2;
then A8:
dom (MIM (R | (n + 1))) = Seg (n + 1)
by FINSEQ_1:def 3;
n + 1 in Seg (n + 1)
by A3;
then
(R | (n + 1)) . (n + 1) = R . (n + 1)
by A1, A5, Th6;
then A9:
(MIM (R | (n + 1))) . (n + 1) = R . (n + 1)
by A6, A7, Def2;
A10:
Seg (len ((MIM R) | n)) = dom ((MIM R) | n)
by FINSEQ_1:def 3;
A11:
Seg (len (MIM R)) = dom (MIM R)
by FINSEQ_1:def 3;
A12:
len (MIM R) = n + 2
by A1, Def2;
then A13:
len ((MIM R) | n) = n
by FINSEQ_1:59, NAT_1:11;
A14:
n <= n + 2
by NAT_1:11;
A15:
now for m being Nat st m in dom (MIM (R | (n + 1))) holds
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . mlet m be
Nat;
( m in dom (MIM (R | (n + 1))) implies (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m )assume A16:
m in dom (MIM (R | (n + 1)))
;
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . mthen A17:
1
<= m
by A8, FINSEQ_1:1;
A18:
m <= n + 1
by A8, A16, FINSEQ_1:1;
now ( ( m = n + 1 & (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m ) or ( m <> n + 1 & (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m ) )per cases
( m = n + 1 or m <> n + 1 )
;
case
m <> n + 1
;
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . mthen A19:
m < n + 1
by A18, XXREAL_0:1;
then A20:
m <= n
by NAT_1:13;
then A21:
m in Seg n
by A17;
set r2 =
R . (m + 1);
set r1 =
R . m;
A22:
(len (MIM R)) - 1
= n + 1
by A12;
1
<= n
by A17, A20, XXREAL_0:2;
then
n in Seg (n + 2)
by A14;
then
((MIM R) | n) . m = (MIM R) . m
by A12, A11, A21, Th6;
then A23:
(R . m) - (R . (m + 1)) =
((MIM R) | n) . m
by A17, A18, A22, Def2
.=
(((MIM R) | n) ^ <*(R . (n + 1))*>) . m
by A13, A10, A21, FINSEQ_1:def 7
;
( 1
<= m + 1 &
m + 1
<= n + 1 )
by A19, NAT_1:11, NAT_1:13;
then
m + 1
in Seg (n + 1)
;
then A24:
(R | (n + 1)) . (m + 1) = R . (m + 1)
by A1, A5, Th6;
(
(len (MIM (R | (n + 1)))) - 1
= n &
(R | (n + 1)) . m = R . m )
by A1, A7, A5, A8, A16, Th6;
hence
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m
by A17, A20, A23, A24, Def2;
verum end; hence
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m
;
verum end;
len (((MIM R) | n) ^ <*(R . (n + 1))*>) =
n + (len <*(R . (n + 1))*>)
by A13, FINSEQ_1:22
.=
n + 1
by FINSEQ_1:40
;
hence
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*(R . (n + 1))*>
by A7, A15, FINSEQ_2:9; verum