Implication Details

Assumptions: kernels, normal, preadditive

Reason: Let $f, g : E \rightrightarrows X$ be a congruence. Then let $E_0$ be the kernel of $g$ . We see that $f|_{E_0} : E_0 \to X$ is a monomorphism. Let $f|_{E_0}$ be the kernel of a morphism $h : X \to Y$ . We claim that $E$ is also the kernel pair of $h$ .
To see this, suppose we have a pair of generalized elements $x_1, x_2 \in X(T)$ . Then we have $\begin{align*} (x_1,x_2) \in E & \iff (x_1 - x_2,0) \in E \\ & \iff x_1 - x_2 \in E_0 \\ & \iff h(x_1 - x_2) = 0 \\ & \iff h(x_1) = h(x_2). \end{align*}$ In particular, applying the forward implications in the case $T := E$ , $x_1 := f$ , $x_2 := g$ , we conclude that $h \circ f = h \circ g$ , so we get the required commutative diagram. From there, the reverse implications show this diagram is a cartesian square.