for X being RealUnitarySpace holds
( X is complete iff RUSp2RNSp X is complete )