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 Th14, RSSPACE:11;
hence 0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, RLSUB_1:11; :: thesis: verum