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

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