for n being Nat
for L being non empty ZeroStr holds seq (n,(0. L)) = 0_. L