theorem Th18: :: LOPBAN_1:18

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