The real-valued part of a point-separating self-adjoint complex function algebra is separating and has the same common zeros

For $f\in A$, self-adjointness and complex linearity put $u:=(f+\bar{f})\mathrm{/}2$ and $v:=(f-\bar{f})\mathrm{/}(2i)$ in $A$.

Sums, real scalar multiples, and products of real-valued members of $A$ are again real-valued by the displayed coordinate formulas in [L2] and [L3], so $A_{\mathbb{R}}$ is a real function algebra by [L1] and [L6]; if $A$ is unital, its real constant functions lie in $A_{\mathbb{R}}$.

The coordinate formulas in [L2], [L3], and [L7] give $u(x)=\mathrm{Re}f(x)$ and $v(x)=\mathrm{Im}f(x)$ for every $x$, so $u$ and $v$ are real-valued. They are continuous as maps into $\mathbb{R}$: each is continuous into $\mathbb{C}$ as a member of $A$, and by [L5] the distance $d_{\mathbb{C}}$ restricted to the real values agrees with $\mathrm{\mid }s-t\mathrm{\mid }$, so the corestriction of a real-valued continuous map to $\mathbb{R}$ is again continuous. Hence $u,v\in C(X,\mathbb{R})$, and [L5] also gives $\mathrm{\mid }u(x)-u(y)\mathrm{\mid }\le d_{\mathbb{C}}(f(x),f(y))$ and $\mathrm{\mid }v(x)-v(y)\mathrm{\mid }\le d_{\mathbb{C}}(f(x),f(y))$.

If $x\mathrm{\ne }y$, choose $f\in A$ with $f(x)\mathrm{\ne }f(y)$. Since $\mathrm{\Phi }$ in [L3] is injective, either $\mathrm{Re}f(x)\mathrm{\ne }\mathrm{Re}f(y)$ or $\mathrm{Im}f(x)\mathrm{\ne }\mathrm{Im}f(y)$, and step 2.1 places the corresponding separator in $A_{\mathbb{R}}$.

If every member of $A$ vanishes at $x$, then every member of $A_{\mathbb{R}}$ does. Conversely, if every member of $A_{\mathbb{R}}$ vanishes at $x$, then step 2.1 makes both real and imaginary parts of every $f(x)$ zero, so coordinate uniqueness in [L2] gives $f(x)=0$; hence the two common-zero sets are equal.