:: deftheorem Def8 defines central_difference VSDIFF_1:def 11 :
for F, G being Field
for V being VectSp of F
for h being Element of V
for W being VectSp of G
for f being PartFunc of V,W
for b₇ being Functional_Sequence of the carrier of V, the carrier of W holds
( b₇ = central_difference (f,h) iff ( b₇ . 0 = f & ( for n being Nat holds b₇ . (n + 1) = cD ((b₇ . n),h) ) ) );