for X being RealNormSpace
for a being Element of REAL
for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
a * x = a * v