Schwartz space and its seminorms

Fix an integer $n\ge 1$. With the complex smooth-function convention of Complex Lp classes and Euclidean test-function conventions and multi-indices of $C^k$ maps and multi-index derivative notation in Euclidean space, define $p_{\alpha \beta }(f)={\sup }_{x\in {\mathbb{R}}^n}\mathrm{\mid }{x}^{\alpha }{\mathrm{\partial }}^{\beta }f(x)\mathrm{\mid },\mathcal{S}({\mathbb{R}}^n)=\{f\in C^{\mathrm{\infty }}({\mathbb{R}}^n;\mathbb{C}):p_{\alpha \beta }(f)<\mathrm{\infty }\text{ for all }\alpha ,\beta \}\mathrm{.}$ The zero multi-index gives $x^0=1$ and ${\mathrm{\partial }}^{0}f=f$. These are actual smooth functions, not equivalence classes. The notation $C_c^{\mathrm{\infty }}$ uses the support convention in The spaces $C_c({\mathbb{R}}^n)$ and $C_c^{\mathrm{\infty }}({\mathbb{R}}^n)$.

Pointwise differentiation is linear; thus $p_{\alpha \beta }(f+g)\le p_{\alpha \beta }(f)+p_{\alpha \beta }(g)$ and $p_{\alpha \beta }(cf)=\mathrm{\mid }c\mathrm{\mid }{p}_{\alpha \beta }(f)$. In particular this set is a complex vector space and each $p_{\alpha \beta }$ is a seminorm. The zero function belongs to it. Since $p_{00}(f)=0$ forces $f(x)=0$ for every $x$, the family separates functions. No choice principle is needed.