Result on D41: Indicator function
Basic real arithmetic expression for cardinality of countable set

Let $X$ be a D16: Countable set.
Then $$|X| = \sum_{x \in X} I_X(x)$$
Also known as
Countable cardinality equals sum of indicator functions
Proofs
<No proofs for this assertion yet>