theorem :: CLOPBAN2:23

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