theorem :: DUALSP01:18

for X being RealNormSpace holds RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is Subspace of X *' by Th22, RSSPACE:11;