:: deftheorem Def7 defines LinearFunctionals DUALSP01:def 6 :
for X being RealLinearSpace
for b₂ being Subset of (RealVectSpace the carrier of X) holds
( b₂ = LinearFunctionals X iff for x being object holds
( x in b₂ iff x is linear-Functional of X ) );