I have a question regarding the terminology in Weil's Basic Number Theory. In Corollary 5 of I-§4 (p. 14) there is a statement regarding division algebras over local fields. It starts like this:
Let $K$ be a commutative $p$-field [nowadays usually called a non-archimedean local field whose residue field is finite and of characteristic $p$], and $K'$ a division algebra over $K$. .....
In the proof, he begins by saying that $K'$ is a finite-dimensional vector space over $K$. Why this is true? Did he simply forget to add 'finite dimensional' or am I missing something? Also I don't see the point why he invokes theorem 5 of I-§3 in the last line.
Thanks in advance, AYK.

These are the statements he is referring to:

The definition of a $p$-field is given by:
