let X, Y be RealLinearSpace; :: thesis: 0. (R_VectorSpace_of_LinearOperators X,Y) = the carrier of X --> (0. Y)
A1: 0. (RealVectSpace the carrier of X,Y) = the carrier of X --> (0. Y) ;
R_VectorSpace_of_LinearOperators X,Y is Subspace of RealVectSpace the carrier of X,Y by Th17, RSSPACE:13;
hence 0. (R_VectorSpace_of_LinearOperators X,Y) = the carrier of X --> (0. Y) by A1, RLSUB_1:19; :: thesis: verum