theorem Th26: :: LOPBAN_9:12

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