theorem Th01: :: VSDIFF_1:2
for F, G being Field
for V being VectSp of F
for W being VectSp of G
for x, h being Element of V
for f being PartFunc of V,W st x in dom f & x + h in dom f holds
(fD (f,h)) /. x = (f /. (x + h)) - (f /. x)