:: deftheorem Def4 defines right_zeroed RLVECT_1:def 4 :
for IT being addLoopStr holds
( IT is right_zeroed iff for v being Element of IT holds v + (0. IT) = v );