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 * (VFuncdiff f1,f2,f3,t0)
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 * (VFuncdiff f1,f2,f3,t0)
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 * (VFuncdiff f1,f2,f3,t0) )
assume A1: ( 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 * (VFuncdiff f1,f2,f3,t0)
set p = |[(diff f1,t0),(diff f2,t0),(diff f3,t0)]|;
A3: ( |[(diff f1,t0),(diff f2,t0),(diff f3,t0)]| . 1 = diff f1,t0 & |[(diff f1,t0),(diff f2,t0),(diff f3,t0)]| . 2 = diff f2,t0 & |[(diff f1,t0),(diff f2,t0),(diff f3,t0)]| . 3 = diff f3,t0 ) by FINSEQ_1:62;
VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = |[(r * (diff f1,t0)),(diff (r (#) f2),t0),(diff (r (#) f3),t0)]| by A1, FDIFF_1:23
.= |[(r * (diff f1,t0)),(r * (diff f2,t0)),(diff (r (#) f3),t0)]| by A1, FDIFF_1:23
.= |[(r * (|[(diff f1,t0),(diff f2,t0),(diff f3,t0)]| . 1)),(r * (|[(diff f1,t0),(diff f2,t0),(diff f3,t0)]| . 2)),(r * (|[(diff f1,t0),(diff f2,t0),(diff f3,t0)]| . 3))]| by A1, A3, FDIFF_1:23
.= r * (VFuncdiff f1,f2,f3,t0) by Lm3 ;
hence VFuncdiff (r (#) f1),(r (#) f2),(r (#) f3),t0 = r * (VFuncdiff f1,f2,f3,t0) ; :: thesis: verum