:: deftheorem Def6 defines forward_difference DIFF_1:def 6 :
for f being PartFunc of REAL,REAL
for h being Real
for b₃ being Functional_Sequence of REAL,REAL holds
( b₃ = forward_difference (f,h) iff ( b₃ . 0 = f & ( for n being Nat holds b₃ . (n + 1) = fD ((b₃ . n),h) ) ) );