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