theorem Th83: :: POLYNOM9:83

for n, m being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + m),L st vars p c= n holds
ex q being Polynomial of n,L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | n in Support q & ( for i being Nat st i >= n holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | n) = p . b ) & ( for x being Function of (n + m),L
for y being Function of n,L st x | n = y holds
eval (p,x) = eval (q,y) ) )