theorem :: DUALSP01:11

for X being RealLinearSpace holds 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))) #) is Subspace of RealVectSpace the carrier of X by Th17, RSSPACE:11;