:: deftheorem Def10 defines accum EUCLID_7:def 10 :
for n being Nat
for f, b₃ being FinSequence of REAL n holds
( b₃ = accum f iff ( len f = len b₃ & f . 1 = b₃ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₃ . (i + 1) = (b₃ /. i) + (f /. (i + 1)) ) ) );