let X, Y be ComplexLinearSpace; :: thesis: 0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)
A1: 0. (ComplexVectSpace ( the carrier of X,Y)) = the carrier of X --> (0. Y) by LOPBAN_1:def 3;
C_VectorSpace_of_LinearOperators (X,Y) is Subspace of ComplexVectSpace ( the carrier of X,Y) by Th15, CSSPACE:13;
hence 0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, CLVECT_1:31; :: thesis: verum