theorem :: LOPBAN_2:21

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