theorem Th3: :: VSDIFF_1:4
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 holds (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)