theorem Th25: :: CLOPBAN1:25

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