for F, G being Field
for V being VectSp of F
for W being VectSp of G
for f being Function of V,W
for x, h being Element of V
for n being Nat st 1. F <> - (1. F) holds
((fdif (f,h)) . (2 * n)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h))