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