let f1, f2, f3 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 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 holds
VFuncdiff (f1 ^ ),(f2 ^ ),(f3 ^ ),t0 = - |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|
let t0 be Real; :: thesis: ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 implies VFuncdiff (f1 ^ ),(f2 ^ ),(f3 ^ ),t0 = - |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| )
assume that
A1: ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 ) and
A2: ( f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 ) ; :: thesis: VFuncdiff (f1 ^ ),(f2 ^ ),(f3 ^ ),t0 = - |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|
set p = |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|;
A4: ( |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| . 1 = (diff f1,t0) / ((f1 . t0) ^2 ) & |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| . 2 = (diff f2,t0) / ((f2 . t0) ^2 ) & |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| . 3 = (diff f3,t0) / ((f3 . t0) ^2 ) ) by FINSEQ_1:62;
VFuncdiff (f1 ^ ),(f2 ^ ),(f3 ^ ),t0 = |[(- ((diff f1,t0) / ((f1 . t0) ^2 ))),(diff (f2 ^ ),t0),(diff (f3 ^ ),t0)]| by A1, A2, FDIFF_2:15
.= |[(- ((diff f1,t0) / ((f1 . t0) ^2 ))),(- ((diff f2,t0) / ((f2 . t0) ^2 ))),(diff (f3 ^ ),t0)]| by A1, A2, FDIFF_2:15
.= |[(- ((diff f1,t0) / ((f1 . t0) ^2 ))),(- ((diff f2,t0) / ((f2 . t0) ^2 ))),(- ((diff f3,t0) / ((f3 . t0) ^2 )))]| by A1, A2, FDIFF_2:15
.= |[((- 1) * (|[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| . 1)),((- 1) * (|[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| . 2)),((- 1) * (|[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| . 3))]| by A4
.= - |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| by Lm3 ;
hence VFuncdiff (f1 ^ ),(f2 ^ ),(f3 ^ ),t0 = - |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]| ; :: thesis: verum