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