for X being RealNormSpace
for x being Point of X
for vseq being sequence of (DualSp X)
for vseq1 being sequence of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st vseq = vseq1 holds
vseq # x = vseq1 # x