:: deftheorem defines | RING_4:def 5 :
for L being non empty ZeroStr
for a being Element of L holds a | L = (0_. L) +* (0,a);