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 Th17;

C_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of C_VectorSpace_of_LinearOperators (X,Y) by Th21, CSSPACE:11;

hence 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, CLVECT_1:30; :: thesis: verum

A1: 0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) by Th17;

C_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of C_VectorSpace_of_LinearOperators (X,Y) by Th21, CSSPACE:11;

hence 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, CLVECT_1:30; :: thesis: verum