:: deftheorem Def3 defines Mult_ CC0SP1:def 3 :
for V being ComplexAlgebra
for V1 being Subset of V st V1 is Cadditively-linearly-closed & not V1 is empty holds
Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:];