theorem :: CLOPBAN2:22

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