let f1, f2, f3, g1, g2, g3 be 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)))]|
let t0 be Real; ( 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 implies 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)))]| )
assume that
A1:
( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 )
and
A2:
( g1 is_differentiable_in f1 . t0 & g2 is_differentiable_in f2 . t0 & g3 is_differentiable_in f3 . t0 )
; 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)))]|
VFuncdiff ((g1 * f1),(g2 * f2),(g3 * f3),t0) =
|[((diff (g1,(f1 . t0))) * (diff (f1,t0))),(diff ((g2 * f2),t0)),(diff ((g3 * f3),t0))]|
by A1, A2, FDIFF_2:13
.=
|[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),(diff ((g3 * f3),t0))]|
by A1, A2, FDIFF_2:13
.=
|[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|
by A1, A2, FDIFF_2:13
;
hence
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)))]|
; verum