to $\cup_{y\in \mu} \max((f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho$, which is in turn equivalent to $\cup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho$.

Summing up, we have thus shown that $$\rho {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\rho \:\Leftrightarrow\: \mu (f(\mu(C))) \cup \textstyle 
\bigcup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho$$ and this, by the above property $(*)$, implies the thesis.

It is important to remark that the above proof basically consists in reducing the equality $f^A = f^B$ between b.c.a.’s to a standard property of completeness of the abstract domains $A$ and $B$ for the function $f$ and then in exploiting the constructive characterization of completeness of abstract domains by Giacobazzi et al. [@grs00 Section 4]. In this sense, the proof itself is particularly interesting because it provides an unexpected reduction of best correct approximations to a completeness problem.

As a consequence of Lemma \[key\] we obtain the following constructive result of existence for correctness kernels. Recall that if $X\subseteq A$ then $\operatorname{Cl}_\wedge (X)$ denotes the glb-closure of $X$ in $A$, while $\operatorname{Cl}_\vee(X)$ denotes the dual lub-closure.

\[kernel\] Let $A \in \operatorname{Abs}(C)$ and $F\subseteq C\rightarrow C$ such that, for any $f\in F$, $f {\circ}\mu_A$ is continuous. Then, the correctness kernel 