:: deftheorem defines \ RING_5:def 2 :
for X being non empty set
for b being bag of X
for a being Element of X holds b \ a = b +* (a,0);