theorem :: LOPBAN_2:23

for X being RealNormSpace holds 1. (R_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;