Double counting: $\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert$ for a relation between finite sets

Let $X$ and $Y$ be finite sets and let $R \subseteq X \times Y$, with row fibres $R_x$ and column fibres $R^{y}$ as in A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_x$ and its column fibres $R^y$. Then, in $\mathbb{N}$,

$\sum_{x \in X}\lvert R_x\rvert \;=\; \lvert R\rvert \;=\; \sum_{y \in Y}\lvert R^{y}\rvert ,$

the sums being those of The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form.

Both index sets may be empty. If $X = \varnothing$ then $R = \varnothing$, every column fibre is empty, and all three quantities are $0$; the same holds with the roles of $X$ and $Y$ exchanged.

• Where the hypotheses are spent. Finiteness of $X$ and of $Y$ is what makes the two index sets legitimate index sets for a sum, and finiteness of $R$ is what makes $\lvert R\rvert$ defined. Disjointness of the slices is automatic, since a slice is determined by one coordinate of its points, which is why no hypothesis of that kind appears in the statement.

• The count stays in $\mathbb{N}$. Every quantity here is a cardinality, and the sums are the $\mathbb{N}$-valued ones. Nothing is embedded into $\mathbb{R}$ until an identity with a subtraction or a division has to be written.