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