I liked the writeup of the problem and the proof quite a bit. I think the $f(x) = x_a$ definition, while it makes sense in context, is a pretty awful abuse of notation, because the author implicitly went from choosing any basis vector a from the Hamel base into fixing a specific a. I think mentioning something like Now fix an $a \in \mathbb{H}$ would be helpful.

It’s too bad that this cool trick isn’t constructive.

I liked the writeup of the problem and the proof quite a bit. I think the

`$f(x) = x_a$`

definition, while it makes sense in context, is a pretty awful abuse of notation, because the author implicitly went from choosing any basis vector`a`

from the Hamel base into fixing a specific`a`

. I think mentioning something like`Now fix an $a \in \mathbb{H}$`

would be helpful.