let X be BCI-algebra; :: thesis: for x, y being Element of X
for m, n being 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 Nat holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y)
let m, n be 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