theorem LM9: :: DUALSP04:23

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