let f1, f2, f3, g1, g2, g3, h1, h2, h3 be 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)))]|
let t0 be Real; ( 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 implies 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)))]| )
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:
( h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0 )
; 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)))]|
A4:
( h3 (#) f3 is_differentiable_in t0 & h1 (#) f1 is_differentiable_in t0 & h2 (#) f2 is_differentiable_in t0 )
by A1, A3, FDIFF_1:16;
then A5:
( (h3 (#) f3) (#) g1 is_differentiable_in t0 & (h3 (#) f3) (#) g2 is_differentiable_in t0 & (h1 (#) f1) (#) g2 is_differentiable_in t0 & (h1 (#) f1) (#) g3 is_differentiable_in t0 & (h2 (#) f2) (#) g3 is_differentiable_in t0 & (h2 (#) f2) (#) g1 is_differentiable_in t0 )
by A2, FDIFF_1:16;
VFuncdiff ((((h2 (#) f2) (#) g3) - ((h3 (#) f3) (#) g2)),(((h3 (#) f3) (#) g1) - ((h1 (#) f1) (#) g3)),(((h1 (#) f1) (#) g2) - ((h2 (#) f2) (#) g1)),t0) =
(VFuncdiff (((h2 (#) f2) (#) g3),((h3 (#) f3) (#) g1),((h1 (#) f1) (#) g2),t0)) - (VFuncdiff (((h3 (#) f3) (#) g2),((h1 (#) f1) (#) g3),((h2 (#) f2) (#) g1),t0))
by A5, Th89
.=
(|[((g3 . t0) * (diff ((h2 (#) f2),t0))),((g1 . t0) * (diff ((h3 (#) f3),t0))),((g2 . t0) * (diff ((h1 (#) f1),t0)))]| + |[(((h2 (#) f2) . t0) * (diff (g3,t0))),(((h3 (#) f3) . t0) * (diff (g1,t0))),(((h1 (#) f1) . t0) * (diff (g2,t0)))]|) - (VFuncdiff (((h3 (#) f3) (#) g2),((h1 (#) f1) (#) g3),((h2 (#) f2) (#) g1),t0))
by A2, A4, Th91
.=
(|[((g3 . t0) * (diff ((h2 (#) f2),t0))),((g1 . t0) * (diff ((h3 (#) f3),t0))),((g2 . t0) * (diff ((h1 (#) f1),t0)))]| + |[(((h2 (#) f2) . t0) * (diff (g3,t0))),(((h3 (#) f3) . t0) * (diff (g1,t0))),(((h1 (#) f1) . t0) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 (#) f3) . t0) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by A2, A4, Th91
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (diff ((h3 (#) f3),t0))),((g2 . t0) * (diff ((h1 (#) f1),t0)))]| + |[(((h2 (#) f2) . t0) * (diff (g3,t0))),(((h3 (#) f3) . t0) * (diff (g1,t0))),(((h1 (#) f1) . t0) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 (#) f3) . t0) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by A1, A3, FDIFF_1:16
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (diff ((h1 (#) f1),t0)))]| + |[(((h2 (#) f2) . t0) * (diff (g3,t0))),(((h3 (#) f3) . t0) * (diff (g1,t0))),(((h1 (#) f1) . t0) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 (#) f3) . t0) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by A1, A3, FDIFF_1:16
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 (#) f2) . t0) * (diff (g3,t0))),(((h3 (#) f3) . t0) * (diff (g1,t0))),(((h1 (#) f1) . t0) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 (#) f3) . t0) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by A1, A3, FDIFF_1:16
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 (#) f3) . t0) * (diff (g1,t0))),(((h1 (#) f1) . t0) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 (#) f3) . t0) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by VALUED_1:5
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 (#) f1) . t0) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 (#) f3) . t0) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by VALUED_1:5
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 (#) f3) . t0) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by VALUED_1:5
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 (#) f1) . t0) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by VALUED_1:5
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 (#) f2) . t0) * (diff (g1,t0)))]|)
by VALUED_1:5
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff ((h3 (#) f3),t0))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 . t0) * (f2 . t0)) * (diff (g1,t0)))]|)
by VALUED_1:5
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g3 . t0) * (diff ((h1 (#) f1),t0))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 . t0) * (f2 . t0)) * (diff (g1,t0)))]|)
by A1, A3, FDIFF_1:16
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g3 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0))))),((g1 . t0) * (diff ((h2 (#) f2),t0)))]| + |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 . t0) * (f2 . t0)) * (diff (g1,t0)))]|)
by A1, A3, FDIFF_1:16
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g3 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0))))),((g1 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0)))))]| + |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 . t0) * (f2 . t0)) * (diff (g1,t0)))]|)
by A1, A3, FDIFF_1:16
.=
((|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) - |[((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g3 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0))))),((g1 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0)))))]|) - |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 . t0) * (f2 . t0)) * (diff (g1,t0)))]|
by RVSUM_1:39
.=
((|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| - |[((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g3 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0))))),((g1 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0)))))]|) + |[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]|) + (- |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 . t0) * (f2 . t0)) * (diff (g1,t0)))]|)
by RVSUM_1:15
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| - |[((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g3 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0))))),((g1 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0)))))]|) + (|[(((h2 . t0) * (f2 . t0)) * (diff (g3,t0))),(((h3 . t0) * (f3 . t0)) * (diff (g1,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g2,t0)))]| - |[(((h3 . t0) * (f3 . t0)) * (diff (g2,t0))),(((h1 . t0) * (f1 . t0)) * (diff (g3,t0))),(((h2 . t0) * (f2 . t0)) * (diff (g1,t0)))]|)
by RVSUM_1:15
.=
(|[((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))),((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))]| - |[((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))),((g3 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0))))),((g1 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,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))))]|
by Lm11
.=
|[((((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))))]| + |[(((g3 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))) - ((g2 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0)))))),(((g1 . t0) * (((f3 . t0) * (diff (h3,t0))) + ((h3 . t0) * (diff (f3,t0))))) - ((g3 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0)))))),(((g2 . t0) * (((f1 . t0) * (diff (h1,t0))) + ((h1 . t0) * (diff (f1,t0))))) - ((g1 . t0) * (((f2 . t0) * (diff (h2,t0))) + ((h2 . t0) * (diff (f2,t0))))))]|
by Lm11
.=
|[((((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))))]| + |[(((((g3 . t0) * (h2 . t0)) * (diff (f2,t0))) - (((g2 . t0) * (h3 . t0)) * (diff (f3,t0)))) + ((((g3 . t0) * (f2 . t0)) * (diff (h2,t0))) - (((g2 . t0) * (f3 . t0)) * (diff (h3,t0))))),(((((g1 . t0) * (h3 . t0)) * (diff (f3,t0))) - (((g3 . t0) * (h1 . t0)) * (diff (f1,t0)))) + ((((g1 . t0) * (f3 . t0)) * (diff (h3,t0))) - (((g3 . t0) * (f1 . t0)) * (diff (h1,t0))))),(((((g2 . t0) * (h1 . t0)) * (diff (f1,t0))) - (((g1 . t0) * (h2 . t0)) * (diff (f2,t0)))) + ((((g2 . t0) * (f1 . t0)) * (diff (h1,t0))) - (((g1 . t0) * (f2 . t0)) * (diff (h2,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))))]| + (|[((((g3 . t0) * (h2 . t0)) * (diff (f2,t0))) - (((g2 . t0) * (h3 . t0)) * (diff (f3,t0)))),((((g1 . t0) * (h3 . t0)) * (diff (f3,t0))) - (((g3 . t0) * (h1 . t0)) * (diff (f1,t0)))),((((g2 . t0) * (h1 . t0)) * (diff (f1,t0))) - (((g1 . t0) * (h2 . t0)) * (diff (f2,t0))))]| + |[((((g3 . t0) * (f2 . t0)) * (diff (h2,t0))) - (((g2 . t0) * (f3 . t0)) * (diff (h3,t0)))),((((g1 . t0) * (f3 . t0)) * (diff (h3,t0))) - (((g3 . t0) * (f1 . t0)) * (diff (h1,t0)))),((((g2 . t0) * (f1 . t0)) * (diff (h1,t0))) - (((g1 . t0) * (f2 . t0)) * (diff (h2,t0))))]|)
by Lm8
.=
(|[((((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))))]| + |[((((g3 . t0) * (h2 . t0)) * (diff (f2,t0))) - (((g2 . t0) * (h3 . t0)) * (diff (f3,t0)))),((((g1 . t0) * (h3 . t0)) * (diff (f3,t0))) - (((g3 . t0) * (h1 . t0)) * (diff (f1,t0)))),((((g2 . t0) * (h1 . t0)) * (diff (f1,t0))) - (((g1 . t0) * (h2 . t0)) * (diff (f2,t0))))]|) + |[((((g3 . t0) * (f2 . t0)) * (diff (h2,t0))) - (((g2 . t0) * (f3 . t0)) * (diff (h3,t0)))),((((g1 . t0) * (f3 . t0)) * (diff (h3,t0))) - (((g3 . t0) * (f1 . t0)) * (diff (h1,t0)))),((((g2 . t0) * (f1 . t0)) * (diff (h1,t0))) - (((g1 . t0) * (f2 . t0)) * (diff (h2,t0))))]|
by RVSUM_1:15
;
hence
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)))]|
; verum