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 unary functions which domain is $F_n$ that satisfies:

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

Then: for any $ \psi \in F_m $ and any set of $ n + m $ functions $ f_1, f_2, \ldots, f_{n+m} \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?