theorem LM10A: :: DUALSP04:24

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