:: deftheorem defines RUSp2RNSp DUALSP04:def 2 :
for X being RealUnitarySpace holds RUSp2RNSp X = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);