for X being RealNormSpace
for x, y being Point of (DualSp X)
for v, w being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v & y = w holds
x + y = v + w