theorem
for
X being non
empty set for
Y being
ComplexNormSpace holds
CLSStruct(#
(ComplexBoundedFunctions (X,Y)),
(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),
(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),
(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is
Subspace of
ComplexVectSpace (
X,
Y)
by Th7, CSSPACE:11;