:: deftheorem Def4 defines permuted_by HILB10_2:def 4 :
for O being Ordinal
for L being non empty ZeroStr
for s being Series of O,L
for perm being Permutation of O
for b₅ being Series of O,L holds
( b₅ = s permuted_by perm iff for b being bag of O holds b₅ . b = s . (b * perm) );