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 = |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| + |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff 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 = |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| + |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff 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 = |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| + |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]|
set p = |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]|;
set q = |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]|;
A4: ( |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| . 1 = (g1 . t0) * (diff f1,t0) & |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| . 2 = (g2 . t0) * (diff f2,t0) & |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| . 3 = (g3 . t0) * (diff f3,t0) ) by FINSEQ_1:62;
A5: ( |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| . 1 = (f1 . t0) * (diff g1,t0) & |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| . 2 = (f2 . t0) * (diff g2,t0) & |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| . 3 = (f3 . t0) * (diff g3,t0) ) by FINSEQ_1:62;
VFuncdiff (f1 (#) g1),(f2 (#) g2),(f3 (#) g3),t0 = |[(((g1 . t0) * (diff f1,t0)) + ((f1 . t0) * (diff g1,t0))),(diff (f2 (#) g2),t0),(diff (f3 (#) g3),t0)]| by A1, A2, FDIFF_1:24
.= |[(((g1 . t0) * (diff f1,t0)) + ((f1 . t0) * (diff g1,t0))),(((g2 . t0) * (diff f2,t0)) + ((f2 . t0) * (diff g2,t0))),(diff (f3 (#) g3),t0)]| by A1, A2, FDIFF_1:24
.= |[((|[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| . 1) + (|[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| . 1)),((|[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| . 2) + (|[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| . 2)),((|[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| . 3) + (|[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| . 3))]| by A1, A2, A4, A5, FDIFF_1:24
.= |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| + |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| by Lm4 ;
hence VFuncdiff (f1 (#) g1),(f2 (#) g2),(f3 (#) g3),t0 = |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| + |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]| ; :: thesis: verum