If $V$ is a finite-dimensional vector space over the field $K$, and if $F$ is a subfield of $K$ such that $[K:F]$ is finite, show that $V$ is a finite-dimensional vector space over $F$ and that moreover $\dim_F V=(\dim_K V) [K:F]$.
I know that $\dim_F V=(\dim_K V) [K:F]$ can be changed into $[V:F]=[V:K][K:F]$, and it is similar to the theorem
Let $F\subseteq K\subseteq V$, then $[V:F]=[V:K][K:F]$.
But is it able to drive the relation $K\subseteq V$?