theorem Th52: :: POLYNOM9:52

for n being Nat
for L being non empty ZeroStr
for p being Series of (n + 1),L holds vars (p removed_last) c= (vars p) \ {n}