Corollary 2

— If E has finite degree over K, then $E_s = \bigcap_{n \geq 0} K(E^{p^n})$.

For each integer $n \geq 0$ denote by F, the subextension $K(E^{p^n})$ of E. The sequence $(F_n)_{n \geq 0}$ of vector subspaces of E is descending and E is of finite dimension over K. Hence there exists an integer $m \geq 0$ such that $F_m = F_n$ for all $n \geq m$. We thus have $K(F_m^p) = F_{m+1} = F_m$, hence $F_m$ is a separable extension of K (V, p. 42, Prop. 11); it is clear that E is p-radical over F, and so Prop. 13 implies $E_s = F_m = \bigcap_{n \geq 0} F_n$.