Orbit indicators form a basis of invariant functions

Write $W$ for the invariant functions. The zero function is invariant. If $f,h\in W$ and $a,b\in k$, then $(af+bh)(g\cdot x)=af(g\cdot x)+bh(g\cdot x)=af(x)+bh(x)=(af+bh)(x)$, so $af+bh\in W$. For each $x$, associativity and commutativity of function addition, the zero and negative identities, $a(f+h)=af+ah$, $(a+b)f=af+bf$, $(ab)f=a(bf)$ and $1_{k}f=f$ are the corresponding field equalities evaluated at $x$. Equality at every $x$ is equality of functions. This verifies all the axioms in F3.

By F2, $x$ and $g\cdot x$ belong to the same orbit. Consequently ${\mathbf{1}}_O(g\cdot x)={\mathbf{1}}_O(x)$, so every orbit indicator lies in $W$. If $f\in W$, its values at any two points of one orbit coincide by F2 and invariance. Each orbit is nonempty, so there is a unique scalar $c_O$ such that $f(x)=c_O$ for all $x\in O$. This defines $c_O$ by its unique value and does not choose orbit representatives.

Define $h={\sum }_{O\in \mathcal{O}}{c}_O{\mathbf{1}}_O$ using F4 in the additive vector space $W$. Evaluation of a finite sum is the sum of its values, by the recursive pointwise addition. At a point $x$, exactly one indicator is $1_k$, namely that of its orbit, and every other term vanishes. Thus $h(x)=c_{G\cdot x}=f(x)$, so $h=f$ and the indicators span $W$.

Suppose ${\sum }_{O\in \mathcal{O}}{a}_O{\mathbf{1}}_O=0$. Fix any orbit $O$ and one $x\in O$, possible because $O$ is nonempty. Evaluation at $x$ gives $a_O=0$. This holds for each orbit separately, so no simultaneous choice is required. Also different orbits have different indicators by evaluation on either orbit and $1_k\mathrm{\ne }{0}_k$. Hence these $\mathrm{\mid }\mathcal{O}\mathrm{\mid }$ vectors are independent and, by F5 and step 2.1, form a basis, giving the asserted dimension.

On $X=G$, set $g\cdot x=gx{g}^{-1}$. Then $ex{e}^{-1}=x$ and $(gh)x(gh{)}^{-1}=g(hx{h}^{-1})g^{-1}$, so this is an action by F1. F6 identifies its orbits as the conjugacy classes. Invariance is precisely constancy on conjugacy classes, the definition of a class function here. If $G$ is finite there are finitely many classes, so steps 1.1–3.1 apply.

If $X=\mathrm{\varnothing }$, there is just the empty function, which is the zero function; there are no orbits and F4 gives the zero function as the empty sum. F5 gives the empty basis and dimension zero. With one orbit, step 2.1 reads $f=c_X{\mathbf{1}}_X$, and step 3.1 proves that this single nonzero indicator is a basis.