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