theorem
for
X,
Y being
ComplexLinearSpace holds
CLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is
Subspace of
ComplexVectSpace ( the
carrier of
X,
Y)
by Th13, CSSPACE:11;