for X being RealNormSpace holds DualSp X is RealNormSpace