let r be Element of REAL ; :: thesis: for f1, f2, f3 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 holds
VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = (((r * (diff f1,t0)) * <e1> ) + ((r * (diff f2,t0)) * <e2> )) + ((r * (diff f3,t0)) * <e3> )
let f1, f2, f3 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 holds
VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = (((r * (diff f1,t0)) * <e1> ) + ((r * (diff f2,t0)) * <e2> )) + ((r * (diff f3,t0)) * <e3> )
let t0 be Real; :: thesis: ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 implies VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = (((r * (diff f1,t0)) * <e1> ) + ((r * (diff f2,t0)) * <e2> )) + ((r * (diff f3,t0)) * <e3> ) )
assume ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 ) ; :: thesis: VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = (((r * (diff f1,t0)) * <e1> ) + ((r * (diff f2,t0)) * <e2> )) + ((r * (diff f3,t0)) * <e3> )
then VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = r * (VFuncdiff f1,f2,f3,t0) by Th59
.= r * ((((diff f1,t0) * <e1> ) + ((diff f2,t0) * <e2> )) + ((diff f3,t0) * <e3> )) by Th29
.= r * ((|[(diff f1,t0),0 ,0 ]| + ((diff f2,t0) * <e2> )) + ((diff f3,t0) * <e3> )) by ThA11
.= r * ((|[(diff f1,t0),0 ,0 ]| + |[0 ,(diff f2,t0),0 ]|) + ((diff f3,t0) * <e3> )) by ThA12
.= r * ((|[(diff f1,t0),0 ,0 ]| + |[0 ,(diff f2,t0),0 ]|) + |[0 ,0 ,(diff f3,t0)]|) by ThA13
.= r * (|[((diff f1,t0) + 0 ),(0 + (diff f2,t0)),(0 + 0 )]| + |[0 ,0 ,(diff f3,t0)]|) by LmA31
.= r * |[((diff f1,t0) + 0 ),((diff f2,t0) + 0 ),(0 + (diff f3,t0))]| by LmA31
.= (((r * (diff f1,t0)) * <e1> ) + ((r * (diff f2,t0)) * <e2> )) + ((r * (diff f3,t0)) * <e3> ) by ThA8 ;
hence VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = (((r * (diff f1,t0)) * <e1> ) + ((r * (diff f2,t0)) * <e2> )) + ((r * (diff f3,t0)) * <e3> ) ; :: thesis: verum