theorem :: BCIALG_5:8

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