theorem Th30: :: CLOPBAN1:30

for X, Y being ComplexNormSpace holds the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y))