theorem Th89:
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 (
(f1 - g1),
(f2 - g2),
(f3 - g3),
t0)
= (VFuncdiff (f1,f2,f3,t0)) - (VFuncdiff (g1,g2,g3,t0))