On a finite compact Hausdorff space a unital separating algebra contains every scalar-valued function

If $X=\mathrm{\varnothing }$, then $F^X$ has only the empty function, which is the zero element of $A$. If $X=\{x\}$, every function is constant, so unitality gives $A=F^X$.

Assume $X$ has at least two points and use [L4] to list its points. For a fixed $x\in X$, [L5] supplies, for each listed $y\mathrm{\ne }x$, a nonempty set of open neighbourhoods of $x$ missing $y$; [L3] chooses one from each member of this finite list. Their intersection is the open singleton $\{x\}$. Hence every singleton is open and every function $X\to F$ is continuous.

For every ordered pair $x\mathrm{\ne }y$, point separation in [L1] or [L2] gives $f_{xy}\in A$ with $f_{xy}(x)\mathrm{\ne }{f}_{xy}(y)$; by [L3] and the finite listing in [L4], choose these over the finite list of ordered pairs and define $h_{xy}:=(f_{xy}-f_{xy}(y))\mathrm{/}(f_{xy}(x)-f_{xy}(y))\in A$. Then $h_{xy}(x)=1$ and $h_{xy}(y)=0$.

For each $x\in X$, the finite product $e_x:={\prod }_{y\mathrm{\ne }x}{h}_{xy}$ belongs to $A$, equals $1$ at $x$, and equals $0$ at every other point because the factor indexed by that point vanishes.

For any function $\phi :X\to F$, the finite sum ${\sum }_{x\in X}\phi (x)e_x$ belongs to $A$ and agrees with $\phi$ at every point. By step 1.2 every such $\phi$ is continuous, so $A=C(X,F)=F^X$.