:: deftheorem Def8 defines central_difference DIFF_1:def 8 :
for f being PartFunc of REAL,REAL
for h being Real
for b₃ being Functional_Sequence of REAL,REAL holds
( b₃ = central_difference (f,h) iff ( b₃ . 0 = f & ( for n being Nat holds b₃ . (n + 1) = cD ((b₃ . n),h) ) ) );