let R be FinSequence of REAL ; :: thesis: for r being Real
for n being Nat st len R = n + 2 & R . (n + 1) = r holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>

let s be Real; :: thesis: for n being Nat st len R = n + 2 & R . (n + 1) = s holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>

let n be Nat; :: thesis: ( len R = n + 2 & R . (n + 1) = s implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> )
assume that
A1: len R = n + 2 and
A2: R . (n + 1) = s ; :: thesis: MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>
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 ;
A6: len (R | (n + 1)) = n + 1 by ;
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 ;
then (R | (n + 1)) . (n + 1) = s by A1, A2, A5, Th6;
then A9: (MIM (R | (n + 1))) . (n + 1) = s 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 ;
then A13: len ((MIM R) | n) = n by ;
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) ^ <*s*>) . m
let m be Nat; :: thesis: ( m in dom (MIM (R | (n + 1))) implies (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m )
assume A16: m in dom (MIM (R | (n + 1))) ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
then A17: 1 <= m by ;
A18: m <= n + 1 by ;
now :: thesis: ( ( m = n + 1 & (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ) or ( m <> n + 1 & (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ) )
per cases ( m = n + 1 or m <> n + 1 ) ;
case m = n + 1 ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by ; :: thesis: verum
end;
case m <> n + 1 ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
then A19: m < n + 1 by ;
then A20: m <= n by NAT_1:13;
then A21: m in Seg n by ;
set r2 = R . (m + 1);
set r1 = R . m;
A22: (len (MIM R)) - 1 = n + 1 by A12;
1 <= n by ;
then n in Seg (n + 2) by ;
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
.= (((MIM R) | n) ^ <*s*>) . m by ;
( 1 <= m + 1 & m + 1 <= n + 1 ) by ;
then m + 1 in Seg (n + 1) by FINSEQ_1: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) ^ <*s*>) . m by A17, A20, A23, A24, Def2; :: thesis: verum
end;
end;
end;
hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ; :: thesis: verum
end;
len (((MIM R) | n) ^ <*s*>) = n + () by
.= n + 1 by FINSEQ_1:40 ;
hence MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> by ; :: thesis: verum