On internal functions and arrows in a Topos I am not an expert on elementary topos (meaning by this to work with the internal language in a Grothendiek topos) and I rather be told than  struggle with the following:
Consider an elementary topos $\mathcal{E}$, a locale $G$, the unique locale morphism 
$i^*: \Omega \to G$, and any arrow $\lambda: X \times Y \to G$:
Consider the following formulae on $\lambda$:
ed): ($\bigvee_{y\in Y} \;\lambda\langle x,y \rangle  = 1$),  
uv): ($\lambda\langle x,y \rangle  \wedge \lambda\langle x,y' \rangle  \leq i^*[[y = y']]$).
Let $\theta: X \times Y \to Map(X,\,Y)$ be the universal locale furnished with such an arrow 
(that is,
 $\forall \lambda \; \exists  ! \; \varphi^* : Map(X,Y) \to G \;\; \varphi^* \theta = \lambda$)
Gavin Wraith in "Localic Groups", Cahiers de 
Top. et Geom. Diff. Vol XXII-1 (1981) defines an object 
$Points(G) = LocalMorphisms(G,\, \Omega) \subset \Omega^G$ and says that it is clear that:
a) $Points(Map(X,\,Y)) = Y^X$.
From this it follows that:
b) There is a bijection $X \times Y \to \Omega \;\equiv\; X \to Y$ 
(where the arrow on the right satisfy ed) and uv))
QUESTION 1] I ask for a convincing proof of a), or better, a proof of the weaker ? b).
Concerning b), consider the following conditions on a relation 
$R \subset X \times Y$:
exed) $\pi_1: R \to X$ is an epimorphism.
exuv) The family $y = \pi_2 (x, y): C \to R \to Y$ is a compatible family with respect to the family $x = \pi_1 (x, y): C \to R \to X$.
(indexed by all $(x, y): C \to R$)
Then, using that epis are strict it follows using standard category theory:
$R$ satisfy exed) and exuv)  $\Leftrightarrow$  $\exists  ! \; f: X \to Y$ such that $R = \Gamma_f$ (the Graph of $f$)
Thus, b) will follow if we can prove :
$R$ satisfy exed) and exuv)  $\Leftrightarrow$ $\varphi_R$ satisfy ed) and uv) ($\varphi_R$ $=$ characteristic function).
This is more related with the formula 
uv'): ($\; \lambda (x, y)  \wedge \lambda ( x', y') \wedge i^*[[x = x']] \leq i [[y = y']] $ )
SUBQUESTION] Are uv) and uv') equivalent ?  
QUESTION 2] 
Consider now a geometric morphism $f: \mathcal{F} \to \mathcal{E}$. We have a bijection 
$X \times Y \to f_*\Omega_\mathcal{E}  \;\; \equiv \;\;  
f^*X \times f^*Y \to \Omega_\mathcal{E}$. 
I want to know if the arrows satisfying ed) and uv) correspond under this bijection.
 A: Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.
Subquestion] these are provably equivalent in first order constructive logic.
Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal E(X\times Y,f_*\Omega)\simeq \mathcal F(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.
A: Thanks, your answer was useful (specially to Question 2) and clarify many things to me, but nevertheless I still am in lack of what I wanted to know in Question 1. 
Question1] ed) means that $\pi_0$ is an epimorphism, less evidently, uv) means that it is a monomorphism. Precisely I would like to have a hint of how to prove this. Out of an internal formula you derive an external statement. I had the statements exed) and exuv) and wanted to know how do you prove that they follow from  ed) and un). I can prove by standard category theory that exed) and exuv) are equivalent to $\pi_0$ being an isomorphism, but I am still in darkness about how using ed) and uv) as hypothesis on $\lambda: X \times Y \to \Omega$, I can  produce an arrow $\lambda: X \to Y$ to work with. Of course, I have a relation $R \subset X \times Y$, and all  I need is to prove that $\pi_0$ is an isomorphism. But, how I can prove (or explain) this ?, more convincingly that writing "it just says so".
Question2] A reference to or proof that the bijection 
$\mathcal{E}(X \times Y, f_* \Omega) \cong \mathcal{F}(f^* X \times f^* Y, \Omega)$ is a locale isomorphism ?. 
Concerning my original question2, it is still necessary to argue how using that being the bijection a locale isomorphism it follows that arrows which satisfy ed) and uv) correspond. 
