:: deftheorem defines Polynom BCIALG_5:def 1 :
for X being BCI-algebra
for x, y being Element of X
for m, n being Nat holds Polynom (m,n,x,y) = (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n;