:: deftheorem defines left_zeroed ALGSTR_1:def 2 :
for IT being non empty addLoopStr holds
( IT is left_zeroed iff for a being Element of IT holds (0. IT) + a = a );