theorem Th92:
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 f1 . t0 &
g2 is_differentiable_in f2 . t0 &
g3 is_differentiable_in f3 . t0 holds
VFuncdiff (
(g1 * f1),
(g2 * f2),
(g3 * f3),
t0)
= |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|