theorem Th20: :: NIVEN:22
for L being non empty ZeroStr
for z being Element of L holds rng <%z%> = {z,(0. L)}