let F, G be Field; 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; 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; 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; 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; ( 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 )
; (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; verum