We prove here that there is just one vector 0 with the property x x+0 = x. First we show that the addition operation for vectors satisfies these axioms for groups where we show that the identity is unique. We have asserted that there are vectors when we declared that there was the at least one 0. Thus c c=c.
To show that vector addition is solvable (ab(c c+a = b ∧ c a+c = b) we note that the c we must seek may be computed as b + (−1)a. We have c+a = (b + (−1)a) + a = b + ((−1)a + a) = b + ((−1)a + 1a) = b + ((−1) + 1)a = b + 0a = b+0 = b. Comutivity of + gives us the rest. Thus we take the symbol “0” to denote that unique vector.