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
B1: ( 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))))]|
A3: ( 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:24;
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 A3, FDIFF_1:22;
B3: (f2 (#) g3) - (f3 (#) g2) is_left_differentiable_in t0 by A5, FDIFF_3:22;
B0: t0 in dom ((f2 (#) g3) - (f3 (#) g2))

proof

consider r being Element of REAL such that
C3: ( 0 < r & [.(t0 - r),t0.] c= dom ((f2 (#) g3) - (f3 (#) g2)) ) by B3, FDIFF_3:def 4;
t0 - r <= t0 by C3, XREAL_1:46;
then t0 in [.(t0 - r),t0.] ;
hence t0 in dom ((f2 (#) g3) - (f3 (#) g2)) by C3; :: thesis: verum

end;

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

proof

consider r1 being Element of REAL such that
C2: ( 0 < r1 & [.(t0 - r1),t0.] c= dom ((f3 (#) g1) - (f1 (#) g3)) ) by B6, FDIFF_3:def 4;
t0 - r1 <= t0 by C2, XREAL_1:46;
then t0 in [.(t0 - r1),t0.] ;
hence t0 in dom ((f3 (#) g1) - (f1 (#) g3)) by C2; :: thesis: verum

end;

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

proof

consider r2 being Element of REAL such that
C1: ( 0 < r2 & [.(t0 - r2),t0.] c= dom ((f1 (#) g2) - (f2 (#) g1)) ) by B8, FDIFF_3:def 4;
t0 - r2 <= t0 by C1, XREAL_1:46;
then t0 in [.(t0 - r2),t0.] ;
hence t0 in dom ((f1 (#) g2) - (f2 (#) g1)) by C1; :: 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 B1, A5, Th60
.= |[((((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 A3, FDIFF_1:22
.= |[((((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 A3, FDIFF_1:22
.= |[((((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 A3, FDIFF_1:22
.= |[((((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:24
.= |[((((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:24
.= |[((((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:24
.= |[((((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:24
.= |[((((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:24
.= |[((((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:24
.= |[((((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 B0, 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 B4, 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 B9, 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 LmA31
.= (|[((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:32 ;
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