:: deftheorem defines DualSp DUALSP01:def 15 :
for X being RealNormSpace holds DualSp X = NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);