\( \newcommand{\cat}[1] {\mathrm{#1}} \newcommand{\catobj}[1] {\operatorname{Obj}(\mathrm{#1})} \newcommand{\cathom}[1] {\operatorname{Hom}_{\cat{#1}}} \)

Series laws Ⅱ: sums over finite sets

9 basic properties of sums over finite sets. The proofs of these are a good exercise to refresh the notions of functions, bijections, sets, sums and induction.

There is 1-1 correspondence between many of these properties and the 6 properties already shown for sums of the form [...]. Thus, proving many of them amounts to choosing a bijection that allows transitioning to one of the original properties.

1. [...]. If \( X \) is empty, and \( f: X \rightarrow \mathbb{R} \) is a function (i.e., \( f \) is the empty function), we have

2. [...]. If \( X \) consists of a single element, \( X = \{x_0\} \), and \( f: X \rightarrow \mathbb{R} \) is a function, we have

3. [...], part I. If \( X \) is a finite set, \( f: X \rightarrow \mathbb{R} \) is a function, and \( g: Y \rightarrow X \) is a bijection, then

4. [...], part II. Let \( n \le m \) be integers, and let \( X \) be the set \( X := \{i \in \mathbb{Z} : n \le i \le m\} \). If \( a_i \) is a real number assigned to each integer \( i \in X \), then we have

5. [...]. Let \( X \), \( Y \) be disjoint finite sets (\( X \cap Y = \emptyset \)), and \( f: X \cup Y \rightarrow \mathbb{R} \) is a function. Then we have

6. [...], part I. Let \( X \) be a finite set, and let \( f: X \rightarrow \mathbb{R} \) and \( g: X \rightarrow \mathbb{R} \) be functions. Then we have

7. [...], part II. Let \( X \) be a finite set, and let \( f: X \rightarrow \mathbb{R} \) be a function, and let \( c \) be a real number. Then

8. [...]. Let \( X \) be a finite set, and let \( f: X \rightarrow \mathbb{R} \) and \( g: X \rightarrow \mathbb{R} \) be functions such that \( f(x) \le g(x) \text{ for all } x \in X \). Then

9. [...]. Let \( X \) be a finite set, and let \( f: X \rightarrow \mathbb{R} \) be a function, then