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 (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

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 (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

let W be VectSp of G; :: thesis: for f being Function of V,W

for x, h being Element of V holds (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

let f be Function of V,W; :: thesis: for x, h being Element of V holds (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

let x, h be Element of V; :: thesis: (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

P1: dom f = the carrier of V by FUNCT_2:def 1;

dom (Shift (f,(- h))) = the carrier of V by FUNCT_2:def 1;

then x in (dom f) /\ (dom (Shift (f,(- h)))) by P1;

then P2: x in dom (f - (Shift (f,(- h)))) by VFUNCT_1:def 2;

thus (bD (f,h)) /. x = (f /. x) - ((Shift (f,(- h))) /. x) by P2, VFUNCT_1:def 2

.= (f /. x) - (f /. (x - h)) by Def2 ; :: thesis: verum

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

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 (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

let W be VectSp of G; :: thesis: for f being Function of V,W

for x, h being Element of V holds (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

let f be Function of V,W; :: thesis: for x, h being Element of V holds (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

let x, h be Element of V; :: thesis: (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

P1: dom f = the carrier of V by FUNCT_2:def 1;

dom (Shift (f,(- h))) = the carrier of V by FUNCT_2:def 1;

then x in (dom f) /\ (dom (Shift (f,(- h)))) by P1;

then P2: x in dom (f - (Shift (f,(- h)))) by VFUNCT_1:def 2;

thus (bD (f,h)) /. x = (f /. x) - ((Shift (f,(- h))) /. x) by P2, VFUNCT_1:def 2

.= (f /. x) - (f /. (x - h)) by Def2 ; :: thesis: verum