Free vector space over a set

You are correct that the condition that $a=b$ if and only if $\alpha_s = \beta_s$ for all $s \in S$ is required. This is wrapped up in definition of a 'formal sum', so I don't think there's any reason why you'd need to spell it out explicitly.

If you wanted to be extremely precise, you could say that the underlying set of $FS$ is the set of functions $a : S \to \mathbb{R}$ such that $\alpha(s) = 0$ for all but finitely many $s \in S$. Writing $\alpha_s = a(s)$ and $\beta_s = b(s)$, the condition that $a=b$ if and only if $\alpha_s=\beta_s$ for all $s \in S$ now follows from the definition of a function, and then you can simply identify the formal sum $a = \sum_{s \in S} \alpha_s s$ with the corresponding function $a : S \to \mathbb{R}$.

(If your vector spaces are over a field $k \ne \mathbb{R}$, that's still fine: just replace $\mathbb{R}$ by $k$ in the previous paragraph.)


A basis of a vector space $V$ is a set $B \subseteq V$ such that for any vector space $W$ and a function $f : B \to W$ there exists a unique linear map $\tilde{f} : V \to W$ which extends $f$.

In your case, let $W$ be a vector space and $f : S \to W$ a function. If a linear map $A : FS \to W$ extends $f$ then by linearity we have

$$A\left(\sum_{s \in S} \alpha_s s\right) = \sum_{s \in S}\alpha A(s) = \sum_{s \in S} \alpha_sf(s)$$

Hence, the only candidate for $\tilde{f} : FS \to W$ is given by $\tilde{f}\left(\sum_{s \in S} \alpha_s s\right) = \sum_{s \in S} \alpha_sf(s)$. This map is indeed linear:

\begin{align} \tilde{f}\left(\lambda\sum_{s \in S} \alpha_s s + \mu\sum_{s \in S} \beta_s s\right) &= \tilde{f}\left(\sum_{s\in S}(\lambda\alpha_s +\mu\beta_s)s \right)\\ &= \sum_{s\in S}(\lambda\alpha_s +\mu\beta_s)f(s)\\ &= \lambda \sum_{s \in S} \alpha_s f(s) + \mu\sum_{s\in S}\beta_s f(s)\\ &= \lambda\tilde{f}\left(\sum_{s \in S} \alpha_s s\right) + \mu\tilde{f}\left(\sum_{s \in S} \beta_s s\right) \end{align}

Therefore $S$ is a basis for $FS$.