rewritting with a new definition of restricted identities

chap-unfixed.tex

@@ -133,8 +133,8 @@ \section{Image and domain}
 ~
 \begin{enumerate}
 \item $\operatorname{IM} f = \setcond{Y \in \mathfrak{Z}}{\mathcal{E}_{\mathcal{C}}^{Y, \Dst f} \circ \mathcal{E}_{\mathcal{C}}^{\Dst f,
-Y} \circ f = f} = \setcond{Y \in \mathfrak{Z}}{\id^{\mathcal{C}(\Dst f,\Dst f)}_{Y\sqcap\Dst f} \circ f = f}$;
-\item $\operatorname{DOM} f = \setcond{X \in \mathfrak{Z}}{f\circ\mathcal{E}_{\mathcal{C}}^{\Src f, X} \circ \mathcal{E}_{\mathcal{C}}^{X, \Src f} = f} = \setcond{X \in \mathfrak{Z}}{f \circ \id^{\mathcal{C}(\Src f,\Src f)}_{X\sqcap\Src f} = f}$.
+Y} \circ f = f} = \setcond{Y \in \mathfrak{Z}}{\id^{\mathcal{C}(\Dst f,\Dst f)}_{[Y]\sqcap[\Dst f]} \circ f = f}$;
+\item $\operatorname{DOM} f = \setcond{X \in \mathfrak{Z}}{f\circ\mathcal{E}_{\mathcal{C}}^{\Src f, X} \circ \mathcal{E}_{\mathcal{C}}^{X, \Src f} = f} = \setcond{X \in \mathfrak{Z}}{f \circ \id^{\mathcal{C}(\Src f,\Src f)}_{[X]\sqcap[\Src f]} = f}$.
 \end{enumerate}
 \end{defn}
 
@@ -156,11 +156,13 @@ \section{Image and domain}
 \end{enumerate}
 \end{prop}
 
+\fxwarning{Not yet rewritten with new definition below this.}
+
 \begin{proof}
 $\operatorname{IM} f =
-\setcond{Y \in \mathfrak{Z}}{\id^{\mathcal{C}(\Dst f,\Dst f)}_{Y\sqcap\Dst f} \circ f = f}$.
+\setcond{Y \in \mathfrak{Z}}{\id^{\mathcal{C}(\Dst f,\Dst f)}_{[Y]\sqcap[\Dst f]} \circ f = f}$.
 
-Suppose $Y\in\operatorname{IM}f$. Then take $Y'=Y\sqcap\Dst f$. We have $Y\sqsupseteq Y'$ and $Y'\in\operatorname{Im}f$. So $Y\in\mathscr{S}\operatorname{Im}f$. If $Y\in\mathscr{S}\operatorname{Im}f$ then $Y\in\operatorname{IM}f$ obviously.
+Suppose $Y\in\operatorname{IM}f$. Then take $Y'=[Y]\sqcap[\Dst f]$. We have $Y\sqsupseteq Y'$ and $Y'\in\operatorname{Im}f$. So $Y\in\mathscr{S}\operatorname{Im}f$. If $Y\in\mathscr{S}\operatorname{Im}f$ then $Y\in\operatorname{IM}f$ obviously.
 So $\operatorname{IM} f = \mathscr{S}\operatorname{Im} f$.
 
 $\rsupfun{\Dst f\cap}\operatorname{IM}f\subseteq