theorem Th26: :: LOPBAN_1:26

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