:: deftheorem Def7 defines Mult_ CSSPACE:def 9 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed holds
Mult_ (X1,X) = the Mult of X | [:COMPLEX,X1:];