let X, Y, Z be RealNormSpace; :: thesis: 0. (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z)
A1: 0. (R_VectorSpace_of_BilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z) by Th18;
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is Subspace of R_VectorSpace_of_BilinearOperators (X,Y,Z) by RSSPACE:11;
hence 0. (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z) by A1, RLSUB_1:11; :: thesis: verum