let F, G be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for x, h being Element of V holds (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)

let x, h be Element of V; :: thesis: (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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: for x, h being Element of V holds (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)

let x, h be Element of V; :: thesis: (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; :: thesis: verum