theorem Th88:
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))