theorem Th31: :: LOPBAN_9:15

for X, Y, Z being RealNormSpace holds the carrier of [:X,Y:] --> (0. Z) = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))