f^B = f^A \;{\Leftrightarrow}\; \operatorname{img}(f^A) \cup \bigcup_{y\in A} 
\max(\{x\in A~|~f^A(x) \leq_A y\}) 
\subseteq B.$$

Let $\mu$ and $\rho$ be the ucos induced by, respectively, the abstractions $A$ and $B$, so that $\mu \sqsubseteq \rho$. Then, observe that $\operatorname{img}(f^A) = \mu(f(\mu(C)))$ and $\{x\in A ~|~ f^A(x) \leq_A y\} = (\mu {\circ}f {\circ}\mu)^{-1}(\downarrow \!y)$. We therefore prove the following equivalent statement which is formalized through ucos: $$\rho {\circ}f {\circ}\rho = \mu {\circ}f {\circ}\mu
\text{~~iff~~}
\mu(f(\mu(C))) \cup \textstyle \bigcup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho.$$ Let us first prove that $$\rho {\circ}f {\circ}\rho = \mu {\circ}f {\circ}\mu \:\Leftrightarrow\: \rho {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\rho\eqno(*)$$\
($\Rightarrow$) On the one hand, $$\begin{aligned}
\mu {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho  & \Rightarrow 
\text{~~~~[by applying $\rho$ to both sides]}
\\
\rho {\circ}\mu {\circ}f {\circ}\mu = \rho{\circ}\rho {\circ}f {\circ}\rho 
& \Rightarrow \text{~~~~[because $\rho {\circ}\rho = \rho$ and 
$\rho {\circ}\mu = \rho$]} \\
\rho  {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho &\Rightarrow \\
\rho  {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu &\end{aligned}$$ and on the other hand, $$\begin{aligned}
\mu {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho  & \Rightarrow 
\text{~~~~[by applying $\rho$ in front to both sides]}
\\
\mu {\circ}f {\circ}\mu {\circ}\rho = \rho{\circ}f {\circ}\rho {\circ}\rho 
& \Rightarrow 
