let X be RealNormSpace; :: thesis: 0. (R_VectorSpace_of_BoundedLinearFunctionals X) = the carrier of X --> 0

A1: 0. (X *') = the carrier of X --> 0 by Th22b;

R_VectorSpace_of_BoundedLinearFunctionals X is Subspace of X *' by Th22, RSSPACE:11;

hence 0. (R_VectorSpace_of_BoundedLinearFunctionals X) = the carrier of X --> 0 by A1, RLSUB_1:11; :: thesis: verum

A1: 0. (X *') = the carrier of X --> 0 by Th22b;

R_VectorSpace_of_BoundedLinearFunctionals X is Subspace of X *' by Th22, RSSPACE:11;

hence 0. (R_VectorSpace_of_BoundedLinearFunctionals X) = the carrier of X --> 0 by A1, RLSUB_1:11; :: thesis: verum