theorem Th14: :: LOPBAN_2:14

for X being RealNormSpace holds Ring_of_BoundedLinearOperators X is Ring