To show that vector addition is solvable (∧a∧b(∨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.