theorem :: DUALSP04:26

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