let F, G be Field; :: thesis: 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)
let V be VectSp of F; :: thesis: 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)
let W be VectSp of G; :: thesis: 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)
let x, h be Element of V; :: thesis: 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)
let f be PartFunc of V,W; :: thesis: ( x in dom f & x + h in dom f implies (fD (f,h)) /. x = (f /. (x + h)) - (f /. x) )
assume A1: ( x in dom f & x + h in dom f ) ; :: thesis: (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)
A2: dom (Shift (f,h)) = (- h) ++ (dom f) by Def1;
(- h) + (x + h) = x + (h + (- h)) by RLVECT_1:def 3
.= x + (0. V) by VECTSP_1:16
.= x by RLVECT_1:def 4 ;
then A4: x in (- h) ++ (dom f) by A1;
A5: (Shift (f,h)) /. x = (Shift (f,h)) . x by A2, A4, PARTFUN1:def 6
.= f . (x + h) by Def1, A4
.= f /. (x + h) by A1, PARTFUN1:def 6 ;
x in (dom (Shift (f,h))) /\ (dom f) by A4, A2, A1, XBOOLE_0:def 4;
then x in dom (fD (f,h)) by VFUNCT_1:def 2;
hence (fD (f,h)) /. x = (f /. (x + h)) - (f /. x) by A5, VFUNCT_1:def 2; :: thesis: verum