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 ((h1 (#) ((f2 (#) g3) - (f3 (#) g2))),(h2 (#) ((f3 (#) g1) - (f1 (#) g3))),(h3 (#) ((f1 (#) g2) - (f2 (#) g1))),t0) = (|[((diff (h1,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))),((diff (h2,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))),((diff (h3,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))]| + |[((h1 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))),((h2 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))),((h3 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))]|) + |[((h1 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))),((h2 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))),((h3 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,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 ((h1 (#) ((f2 (#) g3) - (f3 (#) g2))),(h2 (#) ((f3 (#) g1) - (f1 (#) g3))),(h3 (#) ((f1 (#) g2) - (f2 (#) g1))),t0) = (|[((diff (h1,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))),((diff (h2,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))),((diff (h3,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))]| + |[((h1 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))),((h2 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))),((h3 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))]|) + |[((h1 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))),((h2 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))),((h3 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (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 ) ; :: thesis: VFuncdiff ((h1 (#) ((f2 (#) g3) - (f3 (#) g2))),(h2 (#) ((f3 (#) g1) - (f1 (#) g3))),(h3 (#) ((f1 (#) g2) - (f2 (#) g1))),t0) = (|[((diff (h1,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))),((diff (h2,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))),((diff (h3,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))]| + |[((h1 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))),((h2 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))),((h3 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))]|) + |[((h1 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))),((h2 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))),((h3 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,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: (f2 (#) g3) - (f3 (#) g2) is_left_differentiable_in t0 by FDIFF_3:22;
A7: t0 in dom ((f2 (#) g3) - (f3 (#) g2))

proof

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

end;

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

proof

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

end;

A12: (f1 (#) g2) - (f2 (#) g1) is_left_differentiable_in t0 by A5, FDIFF_3:22;
A13: t0 in dom ((f1 (#) g2) - (f2 (#) g1))

proof

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

end;

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