Prove a simple property of summation I've come across the following fact many times, and I used to take it for granted. However, I cannot think of a both beautiful and rigorous proof of it:

Fact 1:For two non-empty finite sets $A,B$ and map $f:A\times B\to \mathbb R,$ 
  If we have 
  $\big[\exists x_1\neq x_2\in A\times B,\ s.t. f(x_1)=f(x_2)=X\big]\Longrightarrow X=0,$
then we have $\displaystyle\sum_{x\in A}\sum_{y\in B} f(x,y)=\sum_{z\in f(A\times B)} z.$

Question: I know that we can prove this fact using induction, but is there some more beautiful proof of this fact? Thanks in advance.
Edit: I find that this fact also holds when $A,B$ are at most countable sets, and $f\geqslant 0.$
Update: Fact 1 is just a special case of the following fact:

Fact 2: For non-empty finite set $A$ and map $A\to \mathbb R,$ if we have 
  $\big[\exists x_1,x_2\in A,\ s.t. f(x_1)=f(x_2)=X\big]\Longrightarrow X=0,$
  then we have $\displaystyle\sum_{x\in A} f(x)=\sum_{z\in f(A)} z.$



 Proof: According to @Christian Blatter's answer, we have$$\displaystyle\sum_{x\in A} f(x)=\sum_{z\in f(A)-\left\{0\right\}} \mathrm{Card}\big(f^{-1}(z)\big)z,$$   here $f^{-1}(z):=\left\{x\in A|\ f(x)=z\right\}.$     According to the assumption of fact 2, we have $\mathrm{Card}\big(f^{-1}(z)\big)=1$ for each $z\in f(A)-\left\{0\right\}.$ Thus we have$$\displaystyle\sum_{x\in A} f(x)=\sum_{z\in f(A)-\left\{0\right\}} z=\sum_{z\in f(A)} z.$$End of Proof


In addition, the following  fact could be proved similarly:

Fact 3: For two non-empty finite sets $A, B$ and map $\sigma:A\to B,\ \psi:B\to \mathbb R,$ let $f=\psi\circ \sigma,$ denote the set of all zeros of a real-valued function $g$ as $\mathrm{Kel}(g),$ and the image set of a real-valued function $g$ as $\mathrm{Im}(g),$ then 
a) if we have 
  $\big[\exists x_1,x_2\in A,\ s.t. \sigma(x_1)=\sigma(x_2)=X\big]\Longrightarrow X\in \mathrm{Kel}(\psi),$
  then we have $$\displaystyle\sum_{x\in A} f(x)=\sum_{z\in \mathrm{Im}(\sigma)} \psi(z).$$
  b) if we have 
  $\big[\exists x_1,x_2\in B,\ s.t. \psi(x_1)=\psi(x_2)=X\big]\Longrightarrow X=0,$ and $\sigma$ is injective,
  then we have $$\displaystyle\sum_{x\in A} f(x)=\sum_{z\in \psi\big(\mathrm{Im}(\sigma)\big)} z=\sum_{z\in \mathrm{Im}f} z.$$

 A: Since $A$ and $B$ are finite the set $R:=f(A\times B)\subset{\mathbb R}$ is finite as well. It is then obvious that
$$\sum_{(x,y)\in A\times B} f(x,y)=\sum_{z\in R}\bigl|f^{-1}(\{z\})\bigr|\>z=\sum_{z\in R}z\ ,$$
as $\bigl|f^{-1}(\{z\})\bigr|=1$ for all $z\in R\setminus\{0\}$, by assumption.
(Here $\bigl|f^{-1}(\{z\})\bigr|$ denotes the number of pairs $(x,y)$ satisfying $f(x,y)=z$.)
A: Even though the "beauty" of a proof is subjective to a certain degree, I still post my answer using elementary-set-theory.
It suffices to establish a bijection between the support of $f:A \times B \to \Bbb{R}$ (part of the domain which gives nonzero function value) and the nonzero image $f(A\times B)\setminus\{0\}$.  (We ignore the terms $z=f(x,y)=0$, which have no contribution to the sums.)
$$\text{supp}(f):=\{(x,y)\in A\times B \mid f(x,y)\ne0\} \leftrightarrow
\{z \in f(A \times B) \mid z \ne 0\}=f(A\times B)\setminus\{0\}$$
Rewrite the set on the RHS as $\{f(x,y)\in\Bbb{R}\mid x \in A, y \in B, f(x,y)\ne0\}$.  Obviously, the bijection to be constructed is $\tilde{f}:\text{supp}(f) \to f(A\times B)\setminus\{0\}$.  By abuse of notation, we'll denote $\tilde{f}$ (defined on the support of $f$) as $f$.


*

*surjectivity is guaranteed by the very definition of the set on the RHS

*injectivity is assumed: if there are two different elements $(x_1,y_1),(x_2,y_2) \in \text{supp}(f)$ giving the same function value $f(x_1,y_1) = f(x_2,y_2)$, then the assumption in the question implies $f(x_1,y_1)=f(x_2,y_2)=0$, which contradicts the very definition of $\text{supp}(f)$.


Since the sets $A$ and $B$ are finite, so as their direct product $A \times B$.  Finally we have
$$\sum_{(x,y)\in \text{supp}(f)} f(x,y) = \sum_{z\in f(A\times B)\setminus\{0\}} z,$$
which is equivalent to the desired equality.
A: To extend the fact into infinite condition, we assume that at least one of  $A,B$ is countable set, and $f\geqslant 0.$ 
According to the answer by @GUN Supporter, we can prove that 
$\widetilde f:\mathrm{supp}f\to f(A\times B)-\left\{0\right\},\ t\mapsto f(t)$ is bijective, thus for any bijection $\sigma:\mathbb N\to \mathrm{supp} f,$ and any bijection $\tau:\mathbb N\to f(A\times B)-\left\{0\right\},$ just let $\psi=\tau^{-1}\circ \tilde f\circ \sigma,$ then $\psi$ is a bijection, and we have
$$\tilde f\circ \sigma=\tau\circ \psi.$$
Recall the fact that we can change the order of the terms of a positive series freely without affecting its convergence, now we have 
$$\sum_{i=1}^{\infty} \big(\tilde f\circ \sigma\big)(i)=\sum_{i=1}^{\infty}\big(\tau\circ \psi\big)(i)=\sum_{i=1}^{\infty}\tau(i),$$ for any bijection $\sigma,\tau.$ Now we obtain that
$$\sum_{(x,y)\in \mathrm{supp}f}f(x,y)=\sum_{z\in f(A\times B)-\left\{0\right\}} z,$$
or
$$\sum_{x\in A}\sum_{y\in B} f(x,y)=\sum_{z\in f(A\times B)} z.$$
