:: deftheorem defines *' DUALSP01:def 7 :
for X being RealLinearSpace holds X *' = RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #);