:: deftheorem Def6 defines mult_ C0SP1:def 6 :
for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
mult_ (V1,V) = the multF of V || V1;