theorem Th18: :: CLOPBAN2:18

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