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