[proofplan] We prove the strict inequality by showing that no family of at most $\sum_{i \in I}\kappa_i$ functions can exhaust the product $\prod_{i \in I}\lambda_i$. Given such a family $F$, we use the definition of [cardinal sum](/page/Cardinal%20Sum) to inject $F$ into the disjoint union $\bigsqcup_{i \in I}\kappa_i$, thereby partitioning $F$ into pieces $F_i$ of size at most $\kappa_i$. At coordinate $i$, the functions in $F_i$ use fewer than $\operatorname{cf}(\lambda_i)$ many values, so by the definition of [cofinality](/page/Cofinality) these values cannot be cofinal in $\lambda_i$. The [axiom of choice](/page/Axiom%20of%20Choice) selects one missed value at each coordinate, and these choices form a diagonal function outside $F$. [/proofplan] [step:Partition an arbitrary small family of product functions] Let \begin{align*} P := \prod_{i \in I}\lambda_i \end{align*} denote the set of all functions $f: I \to \bigcup_{i \in I}\lambda_i$ such that $f(i) \in \lambda_i$ for every $i \in I$. It is enough to prove that every subset $F \subset P$ with \begin{align*} |F| \leq \sum_{i \in I}\kappa_i \end{align*} is a proper subset of $P$. Fix such a subset $F \subset P$. By the definition of [cardinal sum](/page/Cardinal%20Sum), there exists an injection \begin{align*} e: F \to \bigsqcup_{i \in I}\kappa_i . \end{align*} For each $i \in I$, define \begin{align*} F_i := \{f \in F : e(f) \in \{i\}\times \kappa_i\}. \end{align*} Then $(F_i)_{i \in I}$ is a family of pairwise disjoint subsets of $F$, their union is $F$, and the restriction of $e$ gives an injection $F_i \to \kappa_i$. Hence \begin{align*} |F_i| \leq \kappa_i \end{align*} for every $i \in I$. [guided] The goal is to turn the cardinal estimate on $F$ into coordinate-wise estimates. By the definition of [cardinal sum](/page/Cardinal%20Sum), the cardinal \begin{align*} \sum_{i \in I}\kappa_i \end{align*} is the cardinality of the disjoint union $\bigsqcup_{i \in I}\kappa_i$. Therefore the assumption $|F| \leq \sum_{i \in I}\kappa_i$ gives an injection \begin{align*} e: F \to \bigsqcup_{i \in I}\kappa_i . \end{align*} This injection assigns each function $f \in F$ to one labelled summand $\{i\}\times \kappa_i$. For each $i \in I$, we collect the functions assigned to the $i$-th summand: \begin{align*} F_i := \{f \in F : e(f) \in \{i\}\times \kappa_i\}. \end{align*} These sets are pairwise disjoint because the summands $\{i\}\times \kappa_i$ are pairwise disjoint, and their union is all of $F$ because every $e(f)$ lies in exactly one summand. Moreover, the restriction of $e$ maps $F_i$ injectively into $\{i\}\times\kappa_i$, whose cardinality is $\kappa_i$. Thus \begin{align*} |F_i| \leq \kappa_i \end{align*} for every $i \in I$. This is the point of using the cardinal sum: it lets us distribute the proposed enumeration into pieces small enough for the cofinality hypothesis at each coordinate. [/guided] [/step] [step:Find a value missed at each coordinate] For each $i \in I$, define the coordinate-value set \begin{align*} A_i := \{f(i) : f \in F_i\} \subset \lambda_i . \end{align*} The evaluation map \begin{align*} \operatorname{ev}_i: F_i &\to A_i \\ f &\mapsto f(i) \end{align*} is surjective, so \begin{align*} |A_i| \leq |F_i| \leq \kappa_i < \operatorname{cf}(\lambda_i). \end{align*} By the definition of [cofinality](/page/Cofinality), no subset of $\lambda_i$ of cardinality strictly smaller than $\operatorname{cf}(\lambda_i)$ is cofinal in $\lambda_i$. Hence $A_i$ is not cofinal in $\lambda_i$. Define the set of admissible missed values \begin{align*} M_i := \{\gamma \in \lambda_i : \alpha < \gamma \text{ for every } \alpha \in A_i\}. \end{align*} Since $A_i \subset \lambda_i$ is not cofinal, the set $M_i$ is nonempty. Every element of $M_i$ lies in $\lambda_i$ and is not an element of $A_i$. [guided] Now we inspect only one coordinate at a time. For a fixed $i \in I$, define \begin{align*} A_i := \{f(i) : f \in F_i\} \subset \lambda_i . \end{align*} This is the set of all $i$-th coordinate values used by functions in the $i$-th piece $F_i$. The map \begin{align*} \operatorname{ev}_i: F_i &\to A_i \\ f &\mapsto f(i) \end{align*} is surjective by the definition of $A_i$. Therefore the cardinality of $A_i$ is at most the cardinality of $F_i$: \begin{align*} |A_i| \leq |F_i|. \end{align*} From the previous step, $|F_i| \leq \kappa_i$, and by hypothesis $\kappa_i < \operatorname{cf}(\lambda_i)$. Combining these inequalities gives \begin{align*} |A_i| \leq |F_i| \leq \kappa_i < \operatorname{cf}(\lambda_i). \end{align*} The definition of [cofinality](/page/Cofinality) says that $\operatorname{cf}(\lambda_i)$ is the least cardinality of a cofinal subset of the ordinal $\lambda_i$. Since $A_i$ has cardinality smaller than $\operatorname{cf}(\lambda_i)$, it cannot be cofinal in $\lambda_i$. We record all possible choices rather than choosing one immediately. Define \begin{align*} M_i := \{\gamma \in \lambda_i : \alpha < \gamma \text{ for every } \alpha \in A_i\}. \end{align*} Because $A_i$ is not cofinal in $\lambda_i$, the set $M_i$ is nonempty. If $\gamma \in M_i$, then $\gamma \in \lambda_i$, and the defining inequality $\alpha < \gamma$ for every $\alpha \in A_i$ implies $\gamma \notin A_i$. Thus every element of $M_i$ is a value below $\lambda_i$ missed by the $i$-th coordinates of all functions in $F_i$. [/guided] [/step] [step:Construct the diagonal function outside the family] By the axiom of choice applied to the family of nonempty sets $(M_i)_{i \in I}$, choose a function \begin{align*} \gamma: I &\to \bigcup_{i \in I} M_i \\ i &\mapsto \gamma_i \end{align*} such that $\gamma_i \in M_i$ for every $i \in I$. Define \begin{align*} g: I &\to \bigcup_{i \in I}\lambda_i \\ i &\mapsto \gamma_i . \end{align*} Since $\gamma_i \in M_i \subset \lambda_i$ for every $i \in I$, we have $g \in P$. We claim that $g \notin F$. Let $f \in F$. Since the family $(F_i)_{i \in I}$ covers $F$, there exists $i \in I$ such that $f \in F_i$. Then $f(i) \in A_i$, while $\gamma_i \notin A_i$. Therefore \begin{align*} g(i) = \gamma_i \neq f(i), \end{align*} so $g \neq f$. Since this holds for every $f \in F$, the function $g$ is not in $F$. [guided] We now assemble the missed coordinate values into one function. The previous step produced, for every $i \in I$, a nonempty set $M_i$ of values below $\lambda_i$ that are not used by the $i$-th coordinates of functions in $F_i$. Because $I$ is arbitrary, making one selection from each $M_i$ is exactly where the axiom of choice enters. Applying the axiom of choice to the family $(M_i)_{i \in I}$, choose a function \begin{align*} \gamma: I &\to \bigcup_{i \in I} M_i \\ i &\mapsto \gamma_i \end{align*} such that $\gamma_i \in M_i$ for every $i \in I$. Define \begin{align*} g: I &\to \bigcup_{i \in I}\lambda_i \\ i &\mapsto \gamma_i . \end{align*} For every $i \in I$, the inclusion $M_i \subset \lambda_i$ gives $g(i)=\gamma_i \in \lambda_i$. Hence \begin{align*} g \in \prod_{i \in I}\lambda_i = P. \end{align*} We prove that $g$ is not one of the functions in $F$. Take any $f \in F$. The sets $F_i$ cover $F$, so there is some $i \in I$ with $f \in F_i$. By the definition of $A_i$, this implies \begin{align*} f(i) \in A_i. \end{align*} But $\gamma_i \in M_i$, and every element of $M_i$ lies outside $A_i$, so \begin{align*} g(i) = \gamma_i \neq f(i). \end{align*} Thus $g$ and $f$ differ at coordinate $i$, and therefore $g \neq f$. Since the argument applies to every $f \in F$, no member of $F$ is equal to $g$. [/guided] [/step] [step:Conclude the strict cardinal inequality] We have shown that every subset $F \subset P$ with \begin{align*} |F| \leq \sum_{i \in I}\kappa_i \end{align*} is a proper subset of $P$. Suppose, for contradiction, that \begin{align*} |P| \leq \sum_{i \in I}\kappa_i . \end{align*} Taking $F=P$ would then give a subset $F \subset P$ with $|F| \leq \sum_{i \in I}\kappa_i$ that is not a proper subset of $P$, contradicting the result just proved. Therefore \begin{align*} \sum_{i \in I}\kappa_i < |P| = \prod_{i \in I}\lambda_i . \end{align*} This is the desired inequality. [/step]