Ytukyg

I am following the proof of:

Let $tau$ be a modal similarity type containing only diamonds, and let $phi$ be a $tau$-formula. If $phi$ is satisfiable, then it is satisfiable on a finite model.

I am just proving it for the basic modal language, that is, we only have one diamond $diamond$

The proof is:

Fix a modal formula $phi$ with $deg(phi) = k$. We restrict our modal similarity type $tau$ and our collection of proposition letters to the modal operators and proposition letters actually occurring in $phi$. Let $M_1,w_1$ be such that $M_1,w_1vdash phi$
. By Proposition 2.15, there exists a tree-like model $M_2$ with root $w_2$ such that $M_2,w_2vdash phi$
. Let $M_3 := (M_2 upharpoonright k)$. By Lemma 2.33 we have $M_2,w_2$ is $k$-bisimilar to $M_3 ,w_2$, and by Proposition 2.31 it follows that $M_3,w_2vdash phi$.

The construction of $M_4$ starts here.

By induction on $n le k$ we define finite sets of states $S_0,...,S_k$ and a (final) model $M_4$ with domain $S_0cup cdotscup S_k$; the points in each $S_n$ will have height $n$. Define $S_0$ to be the singleton ${w_2}$. Next, assume that $S_0,...,S_n$ have already been defined. Fix an element $v$ of $S_n$. By Proposition 2.29 there are only finitely many non-equivalent modal formulas whose degree is at most $k$, say $1,..., m$. For each such formula that is of the form $diamond phi$ and holds in $M_3$ at $v$, select a state $u$ from $M_3$ such that $Rvu$ and $M_3,uvdash phi$. Add all these us to $S_n+1$, and repeat this selection process for every state in $S_n$. $S_{n+1}$ is defined as the set of all points that have been selected in this way.

Finally, define $M_4$ as follows. Its domain is $S_0cupcdots S_k$; as each $S_i$ is finite, $M_4$ is finite. The relations and valuation are obtained by restricting the relations and valuation of M3 to the domain of M4. We can prove that $M_4,w_2$ is $k$-bisimilar to $M_3,w_2$.

The last sentence is actually left as an exercise which is not seems to be easy enough to solve within some hours. Could someone please tell me how to prove it (use some relative theorems?) or give some hint please?

The most important question is that: what is the relation defining an $k$-bisimulation here?

Thank you for any help.