:: deftheorem Def1 defines # DUALSP03:def 1 :
for X being RealNormSpace
for g being sequence of (DualSp X)
for x being Point of X
for b₄ being Real_Sequence holds
( b₄ = g # x iff for i being Nat holds b₄ . i = (g . i) . x );