:: deftheorem defines backward_difference VSDIFF_1:def 9 :
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 Function of V,W
for b₇ being Functional_Sequence of the carrier of V, the carrier of W holds
( b₇ = backward_difference (f,h) iff ( b₇ . 0 = f & ( for n being Nat holds b₇ . (n + 1) = bD ((b₇ . n),h) ) ) );