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)))]|
B1:
( h3 (#) f3 is_differentiable_in t0 & h1 (#) f1 is_differentiable_in t0 & h2 (#) f2 is_differentiable_in t0 )
by A1, A3, FDIFF_1:24;
then B2:
( (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:24;
F1:
for R1, R2, R3 being Element of 3 -tuples_on REAL holds (R1 + R2) - R3 = (R1 - R3) + R2
by RVSUM_1:32;
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 B2, Th58
.=
(|[((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, B1, Th60
.=
(|[((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, B1, Th60
.=
(|[((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:24
.=
(|[((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:24
.=
(|[((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:24
.=
(|[((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:24
.=
(|[((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:24
.=
(|[((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:24
.=
((|[((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:60
.=
((|[((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 F1
.=
(|[((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:32
.=
(|[((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 LmA63
.=
|[((((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 LmA63
.=
|[((((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 LmA31
.=
(|[((((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:32
;
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