theorem Th51: :: POLYNOM9:51

for n being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + 1),L
for x being Function of n,L
for y being Function of (n + 1),L st not n in vars p & y | n = x holds
eval ((p removed_last),x) = eval (p,y)