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