theorem Th18: :: HILB10_2:18

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,L
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (p,x) = eval ((p extended_by_0),y)