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 (f1 - g1),(f2 - g2),(f3 - g3),t0 = (VFuncdiff f1,f2,f3,t0) - (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 (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 ) ; :: thesis: 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)]|;
A4: ( |[(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:62;
A5: ( |[(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:62;
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:22
.= |[((diff f1,t0) - (diff g1,t0)),((diff f2,t0) - (diff g2,t0)),(diff (f3 - g3),t0)]| by A1, A2, FDIFF_1:22
.= |[((|[(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, A4, A5, FDIFF_1:22
.= (VFuncdiff f1,f2,f3,t0) - (VFuncdiff g1,g2,g3,t0) by Lm7 ;
hence VFuncdiff (f1 - g1),(f2 - g2),(f3 - g3),t0 = (VFuncdiff f1,f2,f3,t0) - (VFuncdiff g1,g2,g3,t0) ; :: thesis: verum