:: deftheorem defines DualSp DUALSP04:def 12 :
for X being RealUnitarySpace holds DualSp X = NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);