theorem :: LOPBAN_2:16

for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X is BLAlgebra ;