theorem :: CLOPBAN2:21

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