for X being non trivial ComplexNormSpace holds (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1