:: deftheorem Def2 defines MIM RFINSEQ:def 2 :
for R being real-valued FinSequence
for b₂ being FinSequence of REAL holds
( b₂ = MIM R iff ( len b₂ = len R & b₂ . (len b₂) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b₂) - 1 holds
b₂ . n = (R . n) - (R . (n + 1)) ) ) );