theorem Th31: :: LOPBAN_1:31

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