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