theorem Th17: :: CLOPBAN1:17

for X, Y being ComplexLinearSpace holds 0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)