for X being RealUnitarySpace holds DualSp X = DualSp (RUSp2RNSp X)