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