:: deftheorem Def2 defines BidualFunc DUALSP02:def 2 :
for X being RealNormSpace
for b₂ being Function of X,(DualSp (DualSp X)) holds
( b₂ = BidualFunc X iff for x being Point of X holds b₂ . x = BiDual x );