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
.= (f /. x) - (f /. (x - h)) by Def2 ; :: thesis: verum