:: deftheorem defines zeroed RLVECT_1:def 13 :
for L being non empty addLoopStr holds
( L is zeroed iff for a being Element of L holds
( a + (0. L) = a & (0. L) + a = a ) );