let r be Real; 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; 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; ( 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 )
; 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:14;
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, Th89
.=
(r * (VFuncdiff (f1,f2,f3,t0))) - (r * (VFuncdiff (g1,g2,g3,t0)))
by EUCLIDLP:12
;
hence
VFuncdiff ((r (#) (f1 - g1)),(r (#) (f2 - g2)),(r (#) (f3 - g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) - (r * (VFuncdiff (g1,g2,g3,t0)))
; verum