for m, n being Nat
for L being non empty ZeroStr
for x being Element of L st m <> n holds
(seq (n,x)) . m = 0. L