let r be Real; :: thesis: 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 (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = r * |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|
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 (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = r * |[((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 (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = r * |[((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 (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = r * |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|
( r (#) g1 is_differentiable_in f1 . t0 & r (#) g2 is_differentiable_in f2 . t0 & r (#) g3 is_differentiable_in f3 . t0 ) by A2, FDIFF_1:15;
then VFuncdiff (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = |[((diff ((r (#) g1),(f1 . t0))) * (diff (f1,t0))),((diff ((r (#) g2),(f2 . t0))) * (diff (f2,t0))),((diff ((r (#) g3),(f3 . t0))) * (diff (f3,t0)))]| by A1, Th92
.= |[((r * (diff (g1,(f1 . t0)))) * (diff (f1,t0))),((diff ((r (#) g2),(f2 . t0))) * (diff (f2,t0))),((diff ((r (#) g3),(f3 . t0))) * (diff (f3,t0)))]| by A2, FDIFF_1:15
.= |[((r * (diff (g1,(f1 . t0)))) * (diff (f1,t0))),((r * (diff (g2,(f2 . t0)))) * (diff (f2,t0))),((diff ((r (#) g3),(f3 . t0))) * (diff (f3,t0)))]| by A2, FDIFF_1:15
.= |[((r * (diff (g1,(f1 . t0)))) * (diff (f1,t0))),((r * (diff (g2,(f2 . t0)))) * (diff (f2,t0))),((r * (diff (g3,(f3 . t0)))) * (diff (f3,t0)))]| by A2, FDIFF_1:15
.= |[(r * ((diff (g1,(f1 . t0))) * (diff (f1,t0)))),(r * ((diff (g2,(f2 . t0))) * (diff (f2,t0)))),(r * ((diff (g3,(f3 . t0))) * (diff (f3,t0))))]|
.= r * |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]| by Lm6 ;
hence VFuncdiff (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = r * |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]| ; :: thesis: verum