:: deftheorem Def7 defines backward_difference DIFF_1:def 7 :
for f being PartFunc of REAL,REAL
for h being Real
for b₃ being Functional_Sequence of REAL,REAL holds
( b₃ = backward_difference (f,h) iff ( b₃ . 0 = f & ( for n being Nat holds b₃ . (n + 1) = bD ((b₃ . n),h) ) ) );