for V being RealNormSpace st not V is trivial holds
ex F being Point of (DualSp V) st ||.F.|| = 1