Extended Real Addition is Commutative

Theorem

Extended real addition $+_{\overline{\R}}$ is commutative.

That is, for all $x, y \in \overline{\R}$:

$x +_{\overline{\R}} y = y +_{\overline{\R}} x$

whenever at least one of the sides is defined.

Proof

When $x,y \in \R$, then $x +_{\overline{\R}} y = y +_{\overline{\R}} x$ follows from Real Addition is Commutative.

The remaining cases where the expressions are defined, are already imposed in the definition of $+_{\overline{\R}}$.

$\blacksquare$