for X being RealNormSpace holds Ring_of_BoundedLinearOperators X is Ring