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