We also know that for each object $X$ of a topos $\ECat$, the category $\Sl{\ECat}{X}$ of objects above $X$ is again a topos, and that each arrow $f : X \to Y$ determines a functor $\InvImg{f} : \Sl{\ECat}{Y}\to\Sl{\ECat}{X}$ which admits both a left adjoint (written $\Sigma\Sub{f}$) and a right adjoint (written $\Pi\Sub{f}$).
If we consider just the subobjects of $X$, we obtain a Heyting algebra $\Opns{X}$ and the functor $\InvImg{f}$ induces $f\Sup{-1} : \Opns{Y}\to \Opns{X}$, which likewise admits a right adjoint ($\forall\Sub{f}$, induced by $\Pi\Sub{f}$) and a left adjoint (written $\exists\Sub{f}$, defined by taking the image). By the cartesian adjunction, the objects of $\Opns{X}$ amount to points of $\Omega\Sup{X}$ and the action of the last three functors can be described by arrows of the topos. Thus restricting the image of $A\times f$ to a subobject of $A\times X$ amounts to composing the cartesian adjoint of its characteristic function with the arrow $\exists\Sub{f} : \Omega\Sup{X}\to\Omega\Sup{Y}$, which corresponds exactly to the restriction of the image of $\Omega\Sup{X}\times f$ to $\in\Sub{X}\rightarrowtail \Omega\Sup{X}\times X$ (the subobject characterized by evaluation).
I have taken some liberties with the wording involving images in 1.3 [0003] in order to conform with English mathematical usage; for instance, I have translated phrases like “prendre l’image par $f$ d’un sous-objet de $X$” as “restricting the image of $f$ to a subobject of $X$”.
We note that Bénabou writes “adjonction cartésienne” to refer to the product-exponential adjunction $\prn{-}\times X \dashv \prn{-}\Sup{X}$. Although this terminology is not current, we have retained it as “the cartesian adjunction”.
Another aspect of Bénabou’s terminology that we have retained is the use of “adjoint” to mean “adjoint transpose”; for instance, Bénabou speaks of the “cartesian adjoint” $T\times X\to Y$ of a morphism $T\to Y\Sup{X}$.