let r be Element of 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:22;
then VFuncdiff (r (#) (f1 - g1)),(r (#) (f2 - g2)),(r (#) (f3 - g3)),t0 =
r * (VFuncdiff (f1 - g1),(f2 - g2),(f3 - g3),t0)
by Th59
.=
r * ((VFuncdiff f1,f2,f3,t0) - (VFuncdiff g1,g2,g3,t0))
by A1, A2, Th58
.=
(r * (VFuncdiff f1,f2,f3,t0)) - (r * (VFuncdiff g1,g2,g3,t0))
by EUCLIDLP:17
;
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