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