:: deftheorem defines R_VectorSpace_of_BoundedLinearFunctionals DUALSP01:def 11 :
for X being RealNormSpace holds R_VectorSpace_of_BoundedLinearFunctionals X = RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #);