In the above, I don't understand why the author needs to use another theorem to show that $f$ is separable. Theorem 3.4.5 says that in a finite field, say $F$, the Frobenius automorphism gives us $F = F^p$, entailing that every irreducible polynomial in $F[x]$ is separable. My thinking is, if $E$ exhausts all possible $p^n$ distinct roots of $f$, then $f$ just cannot have repeated roots. This is pretty much the last statement in the paragraph. So, was the author being redundant?
You're correct. This is not really needed and you know right away that f is separable. In general, the idea you have outlined is a common and excellent way to show that a polynomial is separable.