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