Double counting: ${\sum }_{x\in X}\mid R_x\mid =\mid R\mid ={\sum }_{y\in Y}\mid R^y\mid$ 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}\mid R_x\mid =\mid R\mid ={\sum }_{y\in Y}\mid R^y\mid ,$

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=\mathrm{\varnothing }$ then $R=\mathrm{\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 $\mid R\mid$ 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.