if the tensor product of a finite field extension and the separable closure over base field is a field, then their intersection is the base field

This is a step in Corollary 3.3.21 in Liu (Algebraic geometry and Arithmetic curve)

In the proof, we have $K/k$ a finite extension, and $k^s$ the separable closure of $k$. And we showed that $K\bigotimes_k k^s$ is a field.

The proof says

Therefore $K\bigotimes_k k^s$ is a field and it contains $(K\cap k^s)\bigotimes_k (K\cap k^s)$. It follows that $K\cap k^s=k$.

And I don't understand why.

In case other conditions are involved, the picture is presented as following:  I have found my desired lemma.

Proposition: Given a strict field extension $k⊊K$ , the tensor product $K⊗_kK$ is not a field. The proof is in the following link.

https://mathoverflow.net/questions/82083/when-is-the-tensor-product-of-two-fields-a-field

To use this lemma it suffices to show $(K\cap k^s)\bigotimes_k(K\cap k^s)$ is a field. Clearly it's an integral domain as a subring of a field. As $K/k$ is a finite extension, so is $K\cap k^s$, thus $(K\cap k^s)\bigotimes_k(K\cap k^s)$ is a finite dimensional $k$-vector space, at the same time, an integral domain. So it's a field.

Then by above proposition, we must have $K\cap k^s=k$.

$K\cap k^s\otimes_kK\cap k^s$ is a finite dimensional algebra defined over the field $K\cap k^s$, it is semi-simple (no nilpotent ideal) Wedderburn theorem implies that it is isomorphic to a sum of matrix algebras $\oplus_i M_{n_i}(k_i)$ where $k_i$ is a subfield of $k$ since it does not have a divisor of zero, we deduce that it is isomorphic to $k_0$ where $k_0$ is a subfield of $k$. Since it contains $k$, we deduce that it is $K\cap k^s$.

https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_d%27Artin-Wedderburn