theorem Th9: :: BCIALG_5:9

for X being BCI-algebra
for x, y being Element of X
for m, n being Nat holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y)