let f1, f2, f3, g1, g2, g3, h1, h2, h3 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 & h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0 holds
VFuncdiff (((h2 (#) ((f1 (#) g2) - (f2 (#) g1))) - (h3 (#) ((f3 (#) g1) - (f1 (#) g3)))),((h3 (#) ((f2 (#) g3) - (f3 (#) g2))) - (h1 (#) ((f1 (#) g2) - (f2 (#) g1)))),((h1 (#) ((f3 (#) g1) - (f1 (#) g3))) - (h2 (#) ((f2 (#) g3) - (f3 (#) g2)))),t0) = (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) - ((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) - ((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) - ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| + |[(((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))) - ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))) - ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))) - ((h2 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))))]|) + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]|
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 & h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0 implies VFuncdiff (((h2 (#) ((f1 (#) g2) - (f2 (#) g1))) - (h3 (#) ((f3 (#) g1) - (f1 (#) g3)))),((h3 (#) ((f2 (#) g3) - (f3 (#) g2))) - (h1 (#) ((f1 (#) g2) - (f2 (#) g1)))),((h1 (#) ((f3 (#) g1) - (f1 (#) g3))) - (h2 (#) ((f2 (#) g3) - (f3 (#) g2)))),t0) = (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) - ((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) - ((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) - ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| + |[(((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))) - ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))) - ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))) - ((h2 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))))]|) + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . 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 ) ; :: thesis: VFuncdiff (((h2 (#) ((f1 (#) g2) - (f2 (#) g1))) - (h3 (#) ((f3 (#) g1) - (f1 (#) g3)))),((h3 (#) ((f2 (#) g3) - (f3 (#) g2))) - (h1 (#) ((f1 (#) g2) - (f2 (#) g1)))),((h1 (#) ((f3 (#) g1) - (f1 (#) g3))) - (h2 (#) ((f2 (#) g3) - (f3 (#) g2)))),t0) = (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) - ((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) - ((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) - ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| + |[(((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))) - ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))) - ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))) - ((h2 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))))]|) + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]|
A4: ( f2 (#) g3 is_differentiable_in t0 & f3 (#) g2 is_differentiable_in t0 & f3 (#) g1 is_differentiable_in t0 & f1 (#) g3 is_differentiable_in t0 & f1 (#) g2 is_differentiable_in t0 & f2 (#) g1 is_differentiable_in t0 ) by A1, A2, FDIFF_1:16;
then A5: ( (f2 (#) g3) - (f3 (#) g2) is_differentiable_in t0 & (f3 (#) g1) - (f1 (#) g3) is_differentiable_in t0 & (f1 (#) g2) - (f2 (#) g1) is_differentiable_in t0 ) by FDIFF_1:14;
then A6: ( h3 (#) ((f2 (#) g3) - (f3 (#) g2)) is_differentiable_in t0 & h3 (#) ((f3 (#) g1) - (f1 (#) g3)) is_differentiable_in t0 & h2 (#) ((f1 (#) g2) - (f2 (#) g1)) is_differentiable_in t0 & h2 (#) ((f2 (#) g3) - (f3 (#) g2)) is_differentiable_in t0 & h1 (#) ((f3 (#) g1) - (f1 (#) g3)) is_differentiable_in t0 & h1 (#) ((f1 (#) g2) - (f2 (#) g1)) is_differentiable_in t0 ) by A3, FDIFF_1:16;
A7: (f1 (#) g2) - (f2 (#) g1) is_left_differentiable_in t0 by A5, FDIFF_3:22;
A8: t0 in dom ((f1 (#) g2) - (f2 (#) g1))

proof

consider r being Real such that
A9: ( 0 < r & [.(t0 - r),t0.] c= dom ((f1 (#) g2) - (f2 (#) g1)) ) by A7, FDIFF_3:def 4;
t0 - r <= t0 by A9, XREAL_1:44;
then t0 in [.(t0 - r),t0.] ;
hence t0 in dom ((f1 (#) g2) - (f2 (#) g1)) by A9; :: thesis: verum

end;

A10: (f2 (#) g3) - (f3 (#) g2) is_left_differentiable_in t0 by A5, FDIFF_3:22;
A11: t0 in dom ((f2 (#) g3) - (f3 (#) g2))

proof

consider r1 being Real such that
A12: ( 0 < r1 & [.(t0 - r1),t0.] c= dom ((f2 (#) g3) - (f3 (#) g2)) ) by A10, FDIFF_3:def 4;
t0 - r1 <= t0 by A12, XREAL_1:44;
then t0 in [.(t0 - r1),t0.] ;
hence t0 in dom ((f2 (#) g3) - (f3 (#) g2)) by A12; :: thesis: verum

end;

A13: (f3 (#) g1) - (f1 (#) g3) is_left_differentiable_in t0 by A5, FDIFF_3:22;
A14: t0 in dom ((f3 (#) g1) - (f1 (#) g3))

proof

consider r2 being Real such that
A15: ( 0 < r2 & [.(t0 - r2),t0.] c= dom ((f3 (#) g1) - (f1 (#) g3)) ) by A13, FDIFF_3:def 4;
t0 - r2 <= t0 by A15, XREAL_1:44;
then t0 in [.(t0 - r2),t0.] ;
hence t0 in dom ((f3 (#) g1) - (f1 (#) g3)) by A15; :: thesis: verum

end;

VFuncdiff (((h2 (#) ((f1 (#) g2) - (f2 (#) g1))) - (h3 (#) ((f3 (#) g1) - (f1 (#) g3)))),((h3 (#) ((f2 (#) g3) - (f3 (#) g2))) - (h1 (#) ((f1 (#) g2) - (f2 (#) g1)))),((h1 (#) ((f3 (#) g1) - (f1 (#) g3))) - (h2 (#) ((f2 (#) g3) - (f3 (#) g2)))),t0) = (VFuncdiff ((h2 (#) ((f1 (#) g2) - (f2 (#) g1))),(h3 (#) ((f2 (#) g3) - (f3 (#) g2))),(h1 (#) ((f3 (#) g1) - (f1 (#) g3))),t0)) - (VFuncdiff ((h3 (#) ((f3 (#) g1) - (f1 (#) g3))),(h1 (#) ((f1 (#) g2) - (f2 (#) g1))),(h2 (#) ((f2 (#) g3) - (f3 (#) g2))),t0)) by A6, Th89
.= (|[((((f1 (#) g2) - (f2 (#) g1)) . t0) * (diff (h2,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h3,t0))),((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (VFuncdiff ((h3 (#) ((f3 (#) g1) - (f1 (#) g3))),(h1 (#) ((f1 (#) g2) - (f2 (#) g1))),(h2 (#) ((f2 (#) g3) - (f3 (#) g2))),t0)) by A3, A5, Th91
.= (|[((((f1 (#) g2) - (f2 (#) g1)) . t0) * (diff (h2,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h3,t0))),((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h3,t0))),((((f1 (#) g2) - (f2 (#) g1)) . t0) * (diff (h1,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A3, A5, Th91
.= (|[((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h2,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h3,t0))),((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h3,t0))),((((f1 (#) g2) - (f2 (#) g1)) . t0) * (diff (h1,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A8, VALUED_1:13
.= (|[((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h2,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h3,t0))),((((f1 (#) g2) - (f2 (#) g1)) . t0) * (diff (h1,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A11, VALUED_1:13
.= (|[((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h2,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) - (f1 (#) g3)) . t0) * (diff (h3,t0))),((((f1 (#) g2) - (f2 (#) g1)) . t0) * (diff (h1,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A14, VALUED_1:13
.= (|[((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h2,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) - (f2 (#) g1)) . t0) * (diff (h1,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A14, VALUED_1:13
.= (|[((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h2,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) - (f3 (#) g2)) . t0) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A8, VALUED_1:13
.= (|[((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h2,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A11, VALUED_1:13
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 (#) g1) . t0)) * (diff (h2,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 (#) g2) . t0)) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 (#) g3) . t0)) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 (#) g1) . t0) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 (#) g3) . t0)) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 (#) g2) . t0) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 (#) g1) . t0)) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 (#) g3) . t0) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 (#) g2) . t0)) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by VALUED_1:5
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h3 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A4, FDIFF_1:14
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h3 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0)))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A4, FDIFF_1:14
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h3 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * (diff (((f3 (#) g1) - (f1 (#) g3)),t0))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A4, FDIFF_1:14
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h3 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * (diff (((f1 (#) g2) - (f2 (#) g1)),t0))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A4, FDIFF_1:14
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h3 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * (diff (((f2 (#) g3) - (f3 (#) g2)),t0)))]|) by A4, FDIFF_1:14
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h3 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A4, FDIFF_1:14
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (diff ((f2 (#) g1),t0)))),((h3 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (diff ((f3 (#) g2),t0)))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (diff ((f1 (#) g3),t0))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0))))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((diff ((f3 (#) g1),t0)) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0))))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (diff ((f1 (#) g3),t0)))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0))))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0)))))),((h1 . t0) * ((diff ((f1 (#) g2),t0)) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0))))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0)))))),((h1 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (diff ((f2 (#) g1),t0)))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0))))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0)))))),((h1 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h2 . t0) * ((diff ((f2 (#) g3),t0)) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0))))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0)))))),((h1 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h2 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (diff ((f3 (#) g2),t0))))]|) by A1, A2, FDIFF_1:16
.= (|[((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h2,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h3,t0))),((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h1,t0)))]| + |[((h2 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h3 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0)))))),((h1 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0))))))]|) - (|[((((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))) * (diff (h3,t0))),((((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))) * (diff (h1,t0))),((((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))) * (diff (h2,t0)))]| + |[((h3 . t0) * ((((g1 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g1,t0)))) - (((g3 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g3,t0)))))),((h1 . t0) * ((((g2 . t0) * (diff (f1,t0))) + ((f1 . t0) * (diff (g2,t0)))) - (((g1 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g1,t0)))))),((h2 . t0) * ((((g3 . t0) * (diff (f2,t0))) + ((f2 . t0) * (diff (g3,t0)))) - (((g2 . t0) * (diff (f3,t0))) + ((f3 . t0) * (diff (g2,t0))))))]|) by A1, A2, FDIFF_1:16
.= ((|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) + ((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))))]| + |[((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))),((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))),((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))]|) - |[((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))),((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))),((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))))]|) - |[(((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h2 . t0) * (((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0))))) + ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| by RVSUM_1:39
.= (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) + ((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))))]| + (|[((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))),((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))),((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))]| - |[((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))),((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))),((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0))))]|)) - |[(((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h2 . t0) * (((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0))))) + ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| by RVSUM_1:15
.= (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) + ((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))))]| + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]|) - |[(((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h2 . t0) * (((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0))))) + ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| by Lm11
.= (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) + ((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))))]| - |[(((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h2 . t0) * (((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0))))) + ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]|) + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]| by RVSUM_1:15
.= |[((((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))) - (((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))))),((((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) + ((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))))) - (((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) + ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))))),((((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) + ((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))) - (((h2 . t0) * (((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0))))) + ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))))))]| + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]| by Lm11
.= |[((((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) - ((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))))) + (((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))) - ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))))),((((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) - ((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))) + (((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))) - ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))))),((((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) - ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))))) + (((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))) - ((h2 . t0) * (((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0)))))))]| + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]|
.= (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) - ((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) - ((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) - ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| + |[(((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))) - ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))) - ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))) - ((h2 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))))]|) + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]| by Lm8 ;
hence VFuncdiff (((h2 (#) ((f1 (#) g2) - (f2 (#) g1))) - (h3 (#) ((f3 (#) g1) - (f1 (#) g3)))),((h3 (#) ((f2 (#) g3) - (f3 (#) g2))) - (h1 (#) ((f1 (#) g2) - (f2 (#) g1)))),((h1 (#) ((f3 (#) g1) - (f1 (#) g3))) - (h2 (#) ((f2 (#) g3) - (f3 (#) g2)))),t0) = (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) - ((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) - ((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) - ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| + |[(((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))) - ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))) - ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))) - ((h2 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))))]|) + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]| ; :: thesis: verum