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:21;
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, Th57
.=
(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))
; verum