for k, n, m being Nat
for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + m),L ex q being Polynomial of ((n + k) + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L
for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (q,XanyY) ) )