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 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))]|
A3: ( 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:23;
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, A3, Th61
.= |[((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:23
.= |[((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:23
.= |[((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:23
.= |[(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 LmA8 ;
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