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 & g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 holds
VFuncdiff (f1 / g1),(f2 / g2),(f3 / g3),t0 = |[((((diff f1,t0) * (g1 . t0)) - ((diff g1,t0) * (f1 . t0))) / ((g1 . t0) ^2 )),((((diff f2,t0) * (g2 . t0)) - ((diff g2,t0) * (f2 . t0))) / ((g2 . t0) ^2 )),((((diff f3,t0) * (g3 . t0)) - ((diff g3,t0) * (f3 . t0))) / ((g3 . t0) ^2 ))]|
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 & g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 implies VFuncdiff (f1 / g1),(f2 / g2),(f3 / g3),t0 = |[((((diff f1,t0) * (g1 . t0)) - ((diff g1,t0) * (f1 . t0))) / ((g1 . t0) ^2 )),((((diff f2,t0) * (g2 . t0)) - ((diff g2,t0) * (f2 . t0))) / ((g2 . t0) ^2 )),((((diff f3,t0) * (g3 . t0)) - ((diff g3,t0) * (f3 . t0))) / ((g3 . t0) ^2 ))]| )
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 ) and
A3: ( g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 ) ; :: thesis: VFuncdiff (f1 / g1),(f2 / g2),(f3 / g3),t0 = |[((((diff f1,t0) * (g1 . t0)) - ((diff g1,t0) * (f1 . t0))) / ((g1 . t0) ^2 )),((((diff f2,t0) * (g2 . t0)) - ((diff g2,t0) * (f2 . t0))) / ((g2 . t0) ^2 )),((((diff f3,t0) * (g3 . t0)) - ((diff g3,t0) * (f3 . t0))) / ((g3 . t0) ^2 ))]|
VFuncdiff (f1 / g1),(f2 / g2),(f3 / g3),t0 = |[((((diff f1,t0) * (g1 . t0)) - ((diff g1,t0) * (f1 . t0))) / ((g1 . t0) ^2 )),(diff (f2 / g2),t0),(diff (f3 / g3),t0)]| by A1, A2, A3, FDIFF_2:14
.= |[((((diff f1,t0) * (g1 . t0)) - ((diff g1,t0) * (f1 . t0))) / ((g1 . t0) ^2 )),((((diff f2,t0) * (g2 . t0)) - ((diff g2,t0) * (f2 . t0))) / ((g2 . t0) ^2 )),(diff (f3 / g3),t0)]| by A1, A2, A3, FDIFF_2:14
.= |[((((diff f1,t0) * (g1 . t0)) - ((diff g1,t0) * (f1 . t0))) / ((g1 . t0) ^2 )),((((diff f2,t0) * (g2 . t0)) - ((diff g2,t0) * (f2 . t0))) / ((g2 . t0) ^2 )),((((diff f3,t0) * (g3 . t0)) - ((diff g3,t0) * (f3 . t0))) / ((g3 . t0) ^2 ))]| by A1, A2, A3, FDIFF_2:14 ;
hence VFuncdiff (f1 / g1),(f2 / g2),(f3 / g3),t0 = |[((((diff f1,t0) * (g1 . t0)) - ((diff g1,t0) * (f1 . t0))) / ((g1 . t0) ^2 )),((((diff f2,t0) * (g2 . t0)) - ((diff g2,t0) * (f2 . t0))) / ((g2 . t0) ^2 )),((((diff f3,t0) * (g3 . t0)) - ((diff g3,t0) * (f3 . t0))) / ((g3 . t0) ^2 ))]| ; :: thesis: verum