let r be 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 t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,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 t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,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 t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 implies VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,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 t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 ) ; :: thesis: VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,t0)))
( f1 + g1 is_differentiable_in t0 & f2 + g2 is_differentiable_in t0 & f3 + g3 is_differentiable_in t0 ) by A1, A2, FDIFF_1:13;
then VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = r * (VFuncdiff ((f1 + g1),(f2 + g2),(f3 + g3),t0)) by Th90
.= r * ((VFuncdiff (f1,f2,f3,t0)) + (VFuncdiff (g1,g2,g3,t0))) by A1, A2, Th88
.= (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,t0))) by EUCLID_4:6 ;
hence VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,t0))) ; :: thesis: verum