let X, Y be ComplexNormSpace; :: thesis: 0. (C_VectorSpace_of_BoundedLinearOperators X,Y) = the carrier of X --> (0. Y)
A1: 0. (C_VectorSpace_of_LinearOperators X,Y) = the carrier of X --> (0. Y) by Th20;
C_VectorSpace_of_BoundedLinearOperators X,Y is Subspace of C_VectorSpace_of_LinearOperators X,Y by Th24, CSSPACE:13;
hence 0. (C_VectorSpace_of_BoundedLinearOperators X,Y) = the carrier of X --> (0. Y) by A1, CLVECT_1:31; :: thesis: verum