Uniqueness of the derivative in locally convex topological vector space I need a hint of proof of uniqueness of the derivative in locally convex topological vector space (it's asserted in Lang's "Introduction to differentiable manifolds").
Define derivative of a function $f: E \to F$ between two topological vector spaces at the point $x_0$ as a linear operator $f'(x_0) \in L(E, F)$ such that ${}^2\!\!f(y) := f(x_0 + y) - f(x_0) - f'(x_0) y$ is tangent to zero (a function $\varphi$ is tangent to zero if for any neighborhood of zero $W \subset F$ there exists a neighborhood of zero $V \subset E$ such that $\varphi(tV) = o(t)W$).
Now suppose that two operators $A_1$ and $A_2$ satisfy the condition of the derviative. I need to prove then that $A_1 = A_2$. It is easy to see that there must be a neighborhood of zero $V \subset E$ such that $(A_1 - A_2)V = 0$, so we have $\operatorname{span}V \subset \ker (A_1 - A_2) \subset E$, so it is sufficient to prove that $\operatorname{span}V = E$. In case of Banach space it is very easy (any non-empty open set must contain a ball), but in a more general case it seems that this attempt fails (consider a discrete space), and I can't see another strategy.
Is the derivative in fact unique or is some condition stronger than what is stated required for it to be unique?
 A: Note that every neighborhood of zero is absorbing, balanced and convex by definition of local convexity, so your argument is already all of it.
If you think about local convexity in terms of semi-norms, it is clear that neighborhoods of zero are absorbing. In the other direction, we want the Minkowski-functionals of a basic system of neighborhoods to be semi-norms generating the topology (in order to have Hahn-Banach at hand). In order for the Minkowski functional of a convex set to be finite everywhere, we need the neighborhoods to be absorbing (the other two conditions already ensure that they are indeed seminorms).
I suggested to use Hahn-Banach. Let $A = A_1 - A_2 \neq 0$. Take $z = Ay = (A_1 - A_2)y \neq 0$ (assuming that $A_1 \neq A_2$). Then by Hahn-Banach we find a continuous linear functional $\phi: F \to \mathbb{K}$ such that $\phi(z) = 1$. I let you finish this alternative proof, using that $\phi \circ A$ is continuous (I suggested this proof before reading your question entirely, there's not much difference).
Note of course that for both these arguments to work, we need that local convexity includes Hausdorff.

Finally, since the topic of the discrete vector space came up. As I convinced you in the comments, this is not a topological vector space, as scalar multiplication is not continuous. There is however a unique finest locally convex topology making a vector space into a topological vector space: simply take the topology generated by all seminorms.
