theorem :: LOPBAN_2:22

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