:: deftheorem Def6 defines Mult_ RSSPACE:def 9 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Mult_ (X1,X) = the Mult of X | [:REAL,X1:];