Prop. 4.0.3 — strict colimits of quasi-complete spaces are quasi-complete

Let $\mathbb K$ be a real-or-complex scalar field (in practice $\mathbb R$ or $\mathbb C$), and let $V$ be a $\mathbb K$-vector space that is also a real vector space with compatible scalar multiplications (multiplying by a real number $r$ is the same as multiplying by $r\in\mathbb K$), carrying a topology in which addition and negation are continuous, scalar multiplication $\mathbb K\times V\to V$ is jointly continuous, and which is Hausdorff. Let $F_0,F_1,\dots$ be $\mathbb K$-subspaces of $V$ forming a strict colimit presentation of $V$. Strict colimit of the sequence of $\mathbb K$-subspaces $F_0,F_1,F_2,\dots$ of $V$ (the bundle's definition): (i) $F_n\subsetneq F_m$ whenever $n<m$; (ii) every $x\in V$ lies in some $F_n$; (iii) for each $n$, $F_n$ is a closed subset of $F_{n+1}$, where $F_{n+1}$ has the subspace topology from $V$; (iv) $V$ is locally convex as a real topological vector space; (v) every subset $U\subseteq V$ that is balanced over $\mathbb K$ (i.e. $cU\subseteq U$ whenever $|c|\le1$) and convex in the real sense, and whose trace $U\cap F_n$ is a neighbourhood of $0$ in $F_n$ (subspace topology from $V$) for every $n$, is a neighbourhood of $0$ in $V$.

Assume each $F_n$, with the subspace topology from $V$, is quasi-complete over $\mathbb K$. Then $V$ is quasi-complete over $\mathbb K$. 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$.