theorem :: VSDIFF_1:29

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) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))