Description: Derive Axiom ax-hvaddid from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)