let R be real-valued FinSequence; :: thesis: for n being Nat st len R = n + 2 holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*(R . (n + 1))*>
let n be Nat; :: thesis: ( len R = n + 2 implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*(R . (n + 1))*> )
assume A1: len R = n + 2 ; :: thesis: 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 :: thesis: for m being Nat st m in dom (MIM (R | (n + 1))) holds
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m

let m be Nat; :: thesis: ( 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))) ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m
then A17: 1 <= m by A8, FINSEQ_1:1;
A18: m <= n + 1 by A8, A16, FINSEQ_1:1;

now :: thesis: ( ( 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 ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m

hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m by A13, A9, FINSEQ_1:42; :: thesis: verum

end;

case m <> n + 1 ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m

then 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; :: thesis: verum

end;

end;

end;

hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*(R . (n + 1))*>) . m ; :: thesis: 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; :: thesis: verum