:: deftheorem Def4 defines right_unital VECTSP_1:def 4 :
for IT being non empty multLoopStr holds
( IT is right_unital iff for x being Element of IT holds x * (1. IT) = x );