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))]|;
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))]|
.= - |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]| by Lm1 ;
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