for L being non empty ZeroStr
for z0 being Element of L holds
( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L ) )