let R be FinSequence of REAL ; :: 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 ;
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 ;
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 ;
A13: m <= n + 2 by ;
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) by FINSEQ_1:44
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by ;
:: thesis: verum
end;
case m <> n + 2 ; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m
then m < n + 2 by ;
then A15: m <= n + 1 by ;
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) by FINSEQ_1:44
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by ; :: thesis: verum
end;
case m <> n + 1 ; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m
then m < n + 1 by ;
then A19: m <= n by NAT_1:13;
then A20: m in Seg n by ;
1 <= n by ;
then A21: n in Seg (n + 2) by ;
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 ;
:: 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 ; :: thesis: verum