theorem LM6: :: DUALSP04:21

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