Recently, I attempted to generalize the fixed-point lemma and proved the following:

Let $ F_n $ be the set of formulas with $ n $ free variables in $PA$. Let $ \mu $ be the smallest set of functions which domain is $F_n$ that satisfies:

$$\forall \sigma\in F_n, ( f(\sigma) = \ulcorner \sigma \urcorner), f(\sigma) \in \mu $$ $$\forall f_1(\sigma)\in\mu, \forall f_2(\sigma)\in\mu, \ldots \forall f_n(\sigma) \in \mu , ( \ulcorner \sigma(f_1(\sigma), f_2(\sigma), \ldots, f_n(\sigma)) \urcorner \in \mu )$$

Then: for any $ \psi \in F_m $ and any set of $ n + m $ functions $ f_1(\sigma), f_2(\sigma), \ldots, f_{n+m}(\sigma) \in \mu $, there exists $ \varphi \in F_n $ such that:

$$ PA\vdash \varphi(f_1(\varphi), \ldots, f_n(\varphi)) \leftrightarrow \psi(f_{n+1}(\varphi), \ldots, f_{n+m}(\varphi)) $$

The proof itself is straightforward, but I am unsure under which existing research this result is covered, that is, what is the limit to which the fixed point lemma can be generalized? Recently, I have been reading C. Smorynski's article "Fixed Point Algebras." Am I heading in the right direction with my research?