§4 — the space of test functions is quasi-complete

For every natural number $n$: consider the space of complex-valued functions on $\mathbb R^n$ (Euclidean space, with coordinates indexed by $\{0,\dots,n-1\}$) that are infinitely differentiable and have compact support, with the open set being all of $\mathbb R^n$. Give it the topology defined in Mathlib for test functions: the finest topology that is a locally convex (real) topological vector space topology and is coarser than the supremum, over all compact $K\subseteq\mathbb R^n$, of the topologies coinduced by the inclusions of the spaces of smooth functions supported in $K$ (each with its usual Fréchet topology of uniform convergence of all derivatives). The statement asserts that this space is quasi-complete over $\mathbb C$. Quasi-complete over $\mathbb K$ (the bundle's definition): for every index type $I$ (in the same universe as the space) carrying a partial order in which any two elements have a common upper bound, and every family $(v_i)_{i\in I}$ whose set of values is von Neumann bounded over $\mathbb K$ and which is Cauchy (for every neighbourhood $N$ of $0$ there is $i_0$ with $v_i-v_j\in N$ for all $i,j\ge i_0$), there is a point $x$ with $v_i-x\in N$ eventually (for all $i\ge$ some $i_0$) for every neighbourhood $N$ of $0$. The case $n=0$ ($\mathbb R^0$ a single point) is included.