let F, G be 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)
let V be 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)
let W be 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)
let f be Function of V,W; for x, h being Element of V holds (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)
let x, h be Element of V; (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)
dom f = the carrier of V
by FUNCT_2:def 1;
hence
(fD (f,h)) /. x = (f /. (x + h)) - (f /. x)
by Th01; verum