:: deftheorem Def6 defines well-unital VECTSP_1:def 6 :
for IT being non empty multLoopStr holds
( IT is well-unital iff for x being Element of IT holds
( x * (1. IT) = x & (1. IT) * x = x ) );