theorem Th24: :: HILB10_2:24

for O being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of O,L
for x being Function of O,L
for S being one-to-one FinSequence of Bags O st rng S = Support p holds
ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )