theorem Th84: :: POLYNOM9:84

for X being Ordinal
for L being non empty ZeroStr
for s being Series of X,L
for perm being Permutation of X holds vars (s permuted_by perm) c= perm .: (vars s)