theorem Th11: :: RFINSEQ:11

for R being FinSequence of REAL
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*>