theorem Th27: :: POLYDIFF:27

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