theorem
for
X,
Y being
RealLinearSpace holds
RLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is
Subspace of
RealVectSpace ( the
carrier of
X,
Y)
by Th14, RSSPACE:11;