theorem Th27: :: HILB10_2:27

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,L ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )