theorem Th91:
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)
= |[((g1 . t0) * (diff (f1,t0))),((g2 . t0) * (diff (f2,t0))),((g3 . t0) * (diff (f3,t0)))]| + |[((f1 . t0) * (diff (g1,t0))),((f2 . t0) * (diff (g2,t0))),((f3 . t0) * (diff (g3,t0)))]|