for n being Nat
for L being non empty ZeroStr
for p being sequence of L holds (p || n) . n = 0. L