let X be BCI-algebra; :: thesis: for x, y being Element of X
for m, n being Element of NAT holds Polynom (m + 1),n,x,y = (Polynom m,n,x,y) \ (x \ y)
let x, y be Element of X; :: thesis: for m, n being Element of NAT holds Polynom (m + 1),n,x,y = (Polynom m,n,x,y) \ (x \ y)
let m, n be Element of NAT ; :: thesis: Polynom (m + 1),n,x,y = (Polynom m,n,x,y) \ (x \ y)
Polynom (m + 1),n,x,y = (x,(y \ x) to_power n),(x \ y) to_power ((m + 1) + 1) by BCIALG_2:11
.= ((x,(y \ x) to_power n),(x \ y) to_power (m + 1)) \ (x \ y) by BCIALG_2:4
.= ((x,(x \ y) to_power (m + 1)),(y \ x) to_power n) \ (x \ y) by BCIALG_2:11 ;
hence Polynom (m + 1),n,x,y = (Polynom m,n,x,y) \ (x \ y) ; :: thesis: verum