for X being RealNormSpace
for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
||.x.|| = ||.v.||