theorem
for
r being
Real for
f1,
f2,
f3,
g1,
g2,
g3 being
PartFunc of
REAL,
REAL for
t0 being
Real st
f1 is_differentiable_in t0 &
f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 &
g1 is_differentiable_in t0 &
g2 is_differentiable_in t0 &
g3 is_differentiable_in t0 holds
VFuncdiff (
(r (#) (f1 - g1)),
(r (#) (f2 - g2)),
(r (#) (f3 - g3)),
t0)
= (r * (VFuncdiff (f1,f2,f3,t0))) - (r * (VFuncdiff (g1,g2,g3,t0)))