let X be BCI-algebra; :: thesis: for x, y being Element of X
for m, n being 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 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 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 Th7
.= ((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