let R be FinSequence of REAL ; :: thesis: for r being Real
for n being Element of 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 Element of NAT st len R = n + 2 & R . (n + 1) = s holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>
let n be Element of NAT ; :: thesis: ( len R = n + 2 & R . (n + 1) = s implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> )
assume A1: ( len R = n + 2 & 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;
A2: (n + 1) + 1 = n + (1 + 1) ;
then A3: n + 1 <= n + 2 by NAT_1:11;
A4: len (R | (n + 1)) = n + 1 by A1, A2, FINSEQ_1:80, NAT_1:11;
then A5: ( len (MIM (R | (n + 1))) = n + 1 & len (MIM R) = n + 2 ) by A1, Def3;
A6: n <= n + 2 by NAT_1:11;
A7: len ((MIM R) | n) = n by A5, FINSEQ_1:80, NAT_1:11;
then A8: len (((MIM R) | n) ^ <*s*>) = n + (len <*s*>) by FINSEQ_1:35
.= n + 1 by FINSEQ_1:57 ;
A9: ( dom (MIM (R | (n + 1))) = Seg (len (MIM (R | (n + 1)))) & Seg (len (R | (n + 1))) = dom (R | (n + 1)) & Seg (len (MIM R)) = dom (MIM R) & Seg (len ((MIM R) | n)) = dom ((MIM R) | n) & Seg (len R) = dom R ) by FINSEQ_1:def 3;
0 < n + 1 by NAT_1:3;
then 0 + 1 <= n + 1 by NAT_1:13;
then A10: ( n + 1 in Seg (n + 2) & n + 1 in Seg (n + 1) ) by A3, FINSEQ_1:3;
then (R | (n + 1)) . (n + 1) = s by A1, A9, Th19;
then A11: (MIM (R | (n + 1))) . (n + 1) = s by A4, A5, Def3;
X: dom (MIM (R | (n + 1))) = Seg (n + 1) by A5, FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom (MIM (R | (n + 1))) implies (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m )
assume A12: m in dom (MIM (R | (n + 1))) ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
then A13: ( 1 <= m & m <= n + 1 ) by X, FINSEQ_1:3;

now

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 A7, A11, FINSEQ_1:59; :: thesis: verum

end;

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

then A14: m < n + 1 by A13, XXREAL_0:1;
then A15: m <= n by NAT_1:13;
then A16: m in Seg n by A13, FINSEQ_1:3;
1 <= n by A13, A15, XXREAL_0:2;
then n in Seg (n + 2) by A6, FINSEQ_1:3;
then A17: ( ((MIM R) | n) . m = (MIM R) . m & m in dom (MIM R) ) by A5, A9, A16, Th19;
A18: (len (MIM R)) - 1 = n + 1 by A5;
set r1 = R . m;
A19: ( 1 <= m + 1 & m + 1 <= n + 2 ) by A2, A13, NAT_1:11, XREAL_1:8;
set r2 = R . (m + 1);
A20: (R . m) - (R . (m + 1)) = ((MIM R) | n) . m by A13, A17, A18, Def3
.= (((MIM R) | n) ^ <*s*>) . m by A7, A9, A16, FINSEQ_1:def 7 ;
A21: (len (MIM (R | (n + 1)))) - 1 = n by A5;
A22: (R | (n + 1)) . m = R . m by A1, A9, A10, A12, Th19, X;
m + 1 <= n + 1 by A14, NAT_1:13;
then m + 1 in Seg (n + 1) by A19, FINSEQ_1:3;
then (R | (n + 1)) . (m + 1) = R . (m + 1) by A1, A9, A10, Th19;
hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by A13, A15, A20, A21, A22, Def3; :: thesis: verum

end;

end;

end;

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

end;

hence MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> by A5, A8, FINSEQ_2:10; :: thesis: verum