let f1, f2, f3, g1, g2, g3 be PartFunc of REAL ,REAL ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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))]| ; :: thesis: verum