theorem :: EUCLID_8:113

for f1, f2, f3, g1, g2, g3, h1, h2, h3 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 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0 holds
VFuncdiff ((((h2 (#) f2) (#) g3) - ((h3 (#) f3) (#) g2)),(((h3 (#) f3) (#) g1) - ((h1 (#) f1) (#) g3)),(((h1 (#) f1) (#) g2) - ((h2 (#) f2) (#) g1)),t0) = (|[((((h2 . t0) * (f2 . t0)) * (diff (g3,t0))) - (((h3 . t0) * (f3 . t0)) * (diff (g2,t0)))),((((h3 . t0) * (f3 . t0)) * (diff (g1,t0))) - (((h1 . t0) * (f1 . t0)) * (diff (g3,t0)))),((((h1 . t0) * (f1 . t0)) * (diff (g2,t0))) - (((h2 . t0) * (f2 . t0)) * (diff (g1,t0))))]| + |[((((h2 . t0) * (diff (f2,t0))) * (g3 . t0)) - (((h3 . t0) * (diff (f3,t0))) * (g2 . t0))),((((h3 . t0) * (diff (f3,t0))) * (g1 . t0)) - (((h1 . t0) * (diff (f1,t0))) * (g3 . t0))),((((h1 . t0) * (diff (f1,t0))) * (g2 . t0)) - (((h2 . t0) * (diff (f2,t0))) * (g1 . t0)))]|) + |[((((diff (h2,t0)) * (f2 . t0)) * (g3 . t0)) - (((diff (h3,t0)) * (f3 . t0)) * (g2 . t0))),((((diff (h3,t0)) * (f3 . t0)) * (g1 . t0)) - (((diff (h1,t0)) * (f1 . t0)) * (g3 . t0))),((((diff (h1,t0)) * (f1 . t0)) * (g2 . t0)) - (((diff (h2,t0)) * (f2 . t0)) * (g1 . t0)))]|