theorem Th94: :: EUCLID_8:103

for f1, f2, f3 being PartFunc of REAL,REAL
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))]|