theorem LM10B: :: DUALSP04:25

for X being RealUnitarySpace holds X *' = (RUSp2RNSp X) *'