The picture above is from Dummit and Foote, Third Edition. Later in the book, we find
Clearly, the condition of equality is not necessary, as seen by taking the polynomial $ f(x) = ( x ^{2} - 2) ( x ^{2} - 2) $, which is not separable, but its splitting field, $ \mathbb{Q} ( \sqrt{2 } ) $ also has two automorphisms, and the degree of extension over $ \mathbb{Q} $ is also $ 2 $.
However, in the book of Abstract Algebra by the author John A. Beachy, Third Edition, we find that
which disagrees with the definition given by Dummit and Foote. I realize that the terminology of Beachy is, according to Wikipedia, old fashioned, but I redid the proof of Proposition 5 with the "old" definition, and it seems that the condition of equality becomes necessary too.
Question. If we use Beachy's definition, does the equality condition in Proposition 5 become if and only if?
Everyone agrees that an irreducible polynomial over a field is separable iff it has distinct roots in an algebraic closure. There is a well-known (standard?!?) lack of agreement as to when to call a reducible polynomial separable.
I prefer Dummit-Foote's definition, though I wish it stated explicitly that the roots are living in an algebraic closure. As in @Bernard's comment, this definition renders the Derivative Criterion valid, and (thus) it is faithfully preserved by base extension: in plainer language that means that if $f \in F[t]$ and $K/F$ is any field extension, then $f$ is separable when regarded as a polynomial over $F$ iff $f$ is separable when regarded as a polynomial over $K$. In Beachy-Blair's definition, this does not work upon passing from any imperfect field to its algebraic closure.
Having said that: I'm not sure I understand your complaint about the proposition in Dummit-Foote. Is it that in the given case the polynomial is not separable according to their definition so the result doesn't apply, but if you used Beachy-Blair's definition you could apply the result? This seems a bit superficial: the result is actually true whenever the finite extension $E/F$ is normal (i.e., the splitting field of some polynomial) and separable, as is a standard result in most field theory texts. If you want to concentrate on polynomials, you can just observe that the splitting field of a polynomial depends only on the largest squarefree polynomial divisor: in other words, if $f = \prod_{i=1}^r p_i^{e_i}$ with each $p_i$ irrreducible, then the splitting field of $f$ is certainly equal to the splitting field of $\prod_{i=1}^r p_i$.
Ah, I found your question. The answer is yes.