for X, Y being RealNormSpace
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds u - (u + v) = - v