let R be real-valued FinSequence; :: thesis: for r, s being Real
for n being Nat st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds
MIM R = ((MIM R) | n) ^ <*(r - s),s*>
let r, s be Real; :: thesis: for n being Nat st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds
MIM R = ((MIM R) | n) ^ <*(r - s),s*>
let n be Nat; :: thesis: ( len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s implies MIM R = ((MIM R) | n) ^ <*(r - s),s*> )
set mf = MIM R;
set nf = (MIM R) | n;
assume that
A1: len R = n + 2 and
A2: R . (n + 1) = r and
A3: R . (n + 2) = s ; :: thesis: MIM R = ((MIM R) | n) ^ <*(r - s),s*>
A4: len (MIM R) = n + 2 by A1, Def2;
then A5: dom (MIM R) = Seg (n + 2) by FINSEQ_1:def 3;
A6: n + (1 + 1) = (n + 1) + 1 ;
then n + 1 <= n + 2 by NAT_1:11;
then A7: n < n + 2 by NAT_1:13;
A8: len ((MIM R) | n) = n by A4, FINSEQ_1:59, NAT_1:11;
then len (((MIM R) | n) ^ <*(r - s),s*>) = n + (len <*(r - s),s*>) by FINSEQ_1:22;
then A9: len (((MIM R) | n) ^ <*(r - s),s*>) = n + 2 by FINSEQ_1:44;
A10: n <= n + 2 by NAT_1:11;

now :: thesis: for m being Nat st m in dom (MIM R) holds
(MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

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

now :: thesis: ( ( m = n + 2 & (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ) or ( m <> n + 2 & (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ) )

per cases ( m = n + 2 or m <> n + 2 ) ;

case A14: m = n + 2 ; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

hence (MIM R) . m = s by A1, A3, A4, Def2
.= <*(r - s),s*> . ((n + 2) - n)
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A7, A14, FINSEQ_1:24 ;
:: thesis: verum

end;

case m <> n + 2 ; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

then m < n + 2 by A13, XXREAL_0:1;
then A15: m <= n + 1 by A6, NAT_1:13;
A16: (len (MIM R)) - 1 = n + 1 by A4;

now :: thesis: ( ( m = n + 1 & (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ) or ( m <> n + 1 & (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ) )

per cases ( m = n + 1 or m <> n + 1 ) ;

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

then A18: n < m by NAT_1:13;
thus (MIM R) . m = r - s by A2, A3, A6, A12, A16, A17, Def2
.= <*(r - s),s*> . ((n + 1) - n)
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A13, A17, A18, FINSEQ_1:24 ; :: thesis: verum

end;

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

then m < n + 1 by A15, XXREAL_0:1;
then A19: m <= n by NAT_1:13;
then A20: m in Seg n by A12;
1 <= n by A12, A19, XXREAL_0:2;
then A21: n in Seg (n + 2) by A10;
A22: dom ((MIM R) | n) = Seg (len ((MIM R) | n)) by FINSEQ_1:def 3;
dom (MIM R) = Seg (len (MIM R)) by FINSEQ_1:def 3;
hence (MIM R) . m = ((MIM R) | n) . m by A4, A20, A21, Th6
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A20, A22, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ; :: thesis: verum

end;

end;

end;

hence (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ; :: thesis: verum

end;

hence MIM R = ((MIM R) | n) ^ <*(r - s),s*> by A4, A9, FINSEQ_2:9; :: thesis: verum