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)))))]|
B1: ( 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;
B2: ( (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 B1, FDIFF_1:22;
B3: ( 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, B2, FDIFF_1:24;
C2: (f1 (#) g2) - (f2 (#) g1) is_left_differentiable_in t0 by B2, FDIFF_3:22;
C3: t0 in dom ((f1 (#) g2) - (f2 (#) g1))

proof

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

end;

C6: (f2 (#) g3) - (f3 (#) g2) is_left_differentiable_in t0 by B2, FDIFF_3:22;
C7: t0 in dom ((f2 (#) g3) - (f3 (#) g2))

proof

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

end;

C10: (f3 (#) g1) - (f1 (#) g3) is_left_differentiable_in t0 by B2, FDIFF_3:22;
C11: t0 in dom ((f3 (#) g1) - (f1 (#) g3))

proof

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

end;

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 (#) ((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 B3, Th58
.= (|[((((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, B2, Th60
.= (|[((((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, B2, Th60
.= (|[((((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 C3, 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 C7, 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 C11, 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 C11, 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 C3, 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 C7, 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 B1, FDIFF_1:22
.= (|[((((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 B1, FDIFF_1:22
.= (|[((((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 B1, FDIFF_1:22
.= (|[((((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 B1, FDIFF_1:22
.= (|[((((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 B1, FDIFF_1:22
.= (|[((((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 B1, FDIFF_1:22
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= (|[((((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:24
.= ((|[(((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:60
.= (|[(((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:32
.= (|[(((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 LmA63
.= (|[(((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 F1
.= |[((((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 LmA63
.= |[((((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 LmA31 ;
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