Inner product space with no ortho-normal basis without choice

Abstract

We prove in ZF that there is an inner product space, in fact, nicely definable with no orthonormal basis.