theorem Th34: :: POLYNOM9:34

for x being object
for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for t being bag of O
for ordP being one-to-one FinSequence of Bags O st rng ordP = Support (p `^ (t . x)) holds
ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )