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 ((f1 + g1),(f2 + g2),(f3 + g3),t0) = (VFuncdiff (f1,f2,f3,t0)) + (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 ((f1 + g1),(f2 + g2),(f3 + g3),t0) = (VFuncdiff (f1,f2,f3,t0)) + (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 ((f1 + g1),(f2 + g2),(f3 + g3),t0) = (VFuncdiff (f1,f2,f3,t0)) + (VFuncdiff (g1,g2,g3,t0))
set p = |[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]|;
set q = |[(diff (g1,t0)),(diff (g2,t0)),(diff (g3,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:45;
A4:
( |[(diff (g1,t0)),(diff (g2,t0)),(diff (g3,t0))]| . 1 = diff (g1,t0) & |[(diff (g1,t0)),(diff (g2,t0)),(diff (g3,t0))]| . 2 = diff (g2,t0) & |[(diff (g1,t0)),(diff (g2,t0)),(diff (g3,t0))]| . 3 = diff (g3,t0) )
by FINSEQ_1:45;
VFuncdiff ((f1 + g1),(f2 + g2),(f3 + g3),t0) =
|[((diff (f1,t0)) + (diff (g1,t0))),(diff ((f2 + g2),t0)),(diff ((f3 + g3),t0))]|
by A1, A2, FDIFF_1:13
.=
|[((diff (f1,t0)) + (diff (g1,t0))),((diff (f2,t0)) + (diff (g2,t0))),(diff ((f3 + g3),t0))]|
by A1, A2, FDIFF_1:13
.=
|[((|[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]| . 1) + (|[(diff (g1,t0)),(diff (g2,t0)),(diff (g3,t0))]| . 1)),((|[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]| . 2) + (|[(diff (g1,t0)),(diff (g2,t0)),(diff (g3,t0))]| . 2)),((|[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]| . 3) + (|[(diff (g1,t0)),(diff (g2,t0)),(diff (g3,t0))]| . 3))]|
by A1, A2, A3, A4, FDIFF_1:13
.=
(VFuncdiff (f1,f2,f3,t0)) + (VFuncdiff (g1,g2,g3,t0))
by Lm2
;
hence
VFuncdiff ((f1 + g1),(f2 + g2),(f3 + g3),t0) = (VFuncdiff (f1,f2,f3,t0)) + (VFuncdiff (g1,g2,g3,t0))
; verum