Theorem 10 of Section 13.3 by symbolic operations in maxima

load(vect);

We can show that |dTT|^2 * |drr|^4 = |drr~ddrr|^2 (lemma to Theorem 10) directly and symbolically.
First define the derivative drr of vector rr symbolically, and declare the vector drr as a function of t.

drr: [dr1,dr2,dr3];

depends(drr,t);

Then calculate ddrr symbolically.

ddrr: diff(drr,t);

|drr~ddrr|^2 can be calculated symbolically, and simplified by ratsimp().

cc: express(drr ~ ddrr);

A: ratsimp(cc.cc);

Define the unit tangent vector TT by drr, and calculate the derivative of TT symbolically.

TT: drr/sqrt(drr.drr);

dTT: diff(TT, t);

|dTT|^2 * |drr|^4 can be calculated symbolically, and simplified by ratsimp().

B: ratsimp((dTT.dTT)*(drr.drr)^2);

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

A - B;

Thus, we have proved the lemma directory.