Type-offset quotient is a real vector space

The set of all functions $\mathcal{G}\to \mathbb{R}$ exists and is a vector space by [F2]. Separation [F4] selects the functions whose support is finite, so $F$ is a set. It contains zero; if $c,d\in F$, then $\mathrm{supp}(c+d)\subseteq \mathrm{supp}(c)\cup \mathrm{supp}(d)$, a finite union, and $\mathrm{supp}(tc)\subseteq \mathrm{supp}(c)$ for every scalar $t$. Thus $F$ is a linear subspace of the function space by [F3], hence a real vector space.

The index sets $\mathcal{G}\times \mathcal{G}$ and ${\mathbb{R}}_{>0}\times \mathcal{G}$ exist by [F4]. Replacement applied to the two displayed relation maps in [F1] gives the set $\mathcal{R}$; each relation vector has support of size at most three and lies in $F$. The family of finite subsets of $\mathcal{R}$ is a subset of its power set, and the coefficient functions on each such finite subset form sets by [F2] and [F4]. Replacement under finite summation therefore gives the set $N\subseteq F$ of all finite linear combinations.

The zero vector is in $N$ as the empty sum. If $u,v\in N$, write each as a finite combination of relation vectors; their sum is the finite combination on the union of those two finite index sets, adding coefficients where an index repeats. For $t\in \mathbb{R}$, $tu$ is obtained by multiplying every coefficient by $t$. Hence $N$ is closed under addition and scalar multiplication and is a linear subspace of $F$ by [F3].

Define $c\sim d$ on $F$ exactly when $c-d\in N$. Since $0\in N$, $N$ is closed under negatives (take scalar $-1$), and under addition, this relation is reflexive, symmetric and transitive. Each class $[c]=\{d\in F:d-c\in N\}$ is a subset of $F$ by separation; replacement on the set $F$ gives the quotient set of these classes.

If $c\sim c^{\mathrm{\prime }}$ and $d\sim d^{\mathrm{\prime }}$, then $(c+d)-(c^{\mathrm{\prime }}+d^{\mathrm{\prime }})=(c-c^{\mathrm{\prime }})+(d-d^{\mathrm{\prime }})\in N$; and for any scalar $t$, $tc-t{c}^{\mathrm{\prime }}=t(c-c^{\mathrm{\prime }})\in N$. Therefore $[c]+[d]:=[c+d]$ and $t[c]:=[tc]$ do not depend on representatives. The quotient map $c\mapsto [c]$ preserves zero, addition and scalar multiplication; applying it to each vector-space identity in $F$ proves all vector-space axioms in $F\mathrm{/}N$. Every generator in $\mathcal{R}$ lies in $N$, so its class is zero and the two displayed relations hold.