let r be Element of 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))]|)
B2: ( r (#) f1 is_differentiable_in t0 & r (#) f2 is_differentiable_in t0 & r (#) f3 is_differentiable_in t0 ) by A1, FDIFF_1:23;
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, B2, Th60
.= |[((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:23
.= |[((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:23
.= |[((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:23
.= |[((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 LmA8
.= (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 LmA8 ;
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