Theorem 3 of Section 13.2 by symbolic operations in maxima

load(vect);

We can show the differentiation rules directly and symbolically.

First define vectors uu and vv symbolically.

uu: [u1,u2,u3];

vv: [v1,v2,v3];

Then we have to declare that the vectors uu and vv are functions of t.

depends(uu,t);

depends(vv,t);

The dot product and the cross product can be carried out symbolically.

uu . vv;

express(uu ~ vv);

The derivative of the dot product can be calculated symbolically.

dd: diff(uu.vv, t);

The right-hand side of the formula can be similarly calculated symbolically.

ee: diff(uu,t).vv + uu.diff(vv,t);

To see that the left-hand side equals the right-hand side, you can find their difference equal to zero vector.

dd - ee;

Similarly we can differentiate the cross product symbolically.

dd: diff(express(uu~vv),t);

ee: express(diff(uu,t)~vv + uu~diff(vv,t));

dd - ee;

Thus, we have proved the differentiation rules directory.