of $A$ for $F$ exists and it is $$\mathscr{K}_F(A) = \operatorname{Cl_\wedge}\Big(\bigcup_{f\in F}\textstyle \operatorname{img}(f^A) \cup  \bigcup_{y\in \operatorname{img}(f^A)} 
\max(\{x\in A~|~f^A(x) = y\})\Big).$$

Let $\mu = \mu_A$. We prove the following equivalent statement formalized through ucos: $\operatorname{Cl_\wedge}\left(\bigcup_{f\in F} \bigcup_{y\in \mu(f(\mu(C)))} \left(\{y\} \cup \max(\{x\in \mu~|~\mu(f(x)) = y\})\right)\right)$ is the correctness kernel of $\mu$ for $F$.

Let $\rho_\mu \triangleq
\operatorname{Cl_\wedge}\left( \mu(f(\mu(C))) \cup \textstyle \bigcup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\right)$. By Lemma \[key\], we have that $\sqcup \{\rho \in \operatorname{uco}(C)~|~ \rho \sqsupseteq \mu,\: 
\rho {\circ}f {\circ}\rho =  \mu {\circ}f {\circ}\mu\} =
\rho_\mu$. Since $\sqcup \{\rho \in \operatorname{uco}(C)~|~ \rho \sqsupseteq \mu,\: 
\rho {\circ}f {\circ}\rho =  \mu {\circ}f {\circ}\mu\} = 
\sqcup \{\rho \in \operatorname{uco}(C)~|~ 
\rho {\circ}f {\circ}\rho =  \mu {\circ}f {\circ}\mu\}$, as a consequence we also have that $\rho_\mu$ is the correctness kernel of $\mu$ for $F$.\
Therefore, let us prove that $$\begin{gathered}
\operatorname{Cl_\wedge}\left( \mu(f(\mu(C))) \cup \cup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\right) =\\
\textstyle \operatorname{Cl_\wedge}\left( \bigcup_{f\in F} \bigcup_{y\in \mu(f(\mu(C)))} \left(\{y\} \cup \max(\{x\in \mu~|~\mu(f(x)) = y\})\right) \right).\end{gathered}$$ Let us first observe that for any $y\in \mu$, if $z\in \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))$ then $z\in\mu$: in fact, $\mu(f(\mu(\mu(z)))) = \mu(f(\mu(z))) \leq y$, so that from $z \leq \mu(z)$, by maximality of $z$, we get $z=\mu(z)$.\
$(\subseteq)$: Consider $y\in \mu$ and 