let i, j, m, n be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n
for x, y being Element of X holds x,y to_power (j + 1) = x,y to_power (m + 1)
let X be BCK-algebra of i,j,m,n; :: thesis: for x, y being Element of X holds x,y to_power (j + 1) = x,y to_power (m + 1)
let x, y be Element of X; :: thesis: x,y to_power (j + 1) = x,y to_power (m + 1)
A1: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then A2: Polynom (i + 1),j,(x \ y),x = (x \ y),(x \ (x \ y)) to_power j by BCIALG_2:5
.= (x \ (x \ (x \ y))),(x \ (x \ y)) to_power j by BCIALG_1:8
.= (x,(x \ (x \ y)) to_power 1),(x \ (x \ y)) to_power j by BCIALG_2:2
.= x,(x \ (x \ y)) to_power (j + 1) by BCIALG_2:10
.= x,y to_power (j + 1) by BCIALG_2:8 ;
A3: X is BCI-algebra of i + 1,j,m,n + 1 by Th14;
Polynom m,(n + 1),x,(x \ y) = x,(x \ (x \ y)) to_power (m + 1) by A1, BCIALG_2:5
.= x,y to_power (m + 1) by BCIALG_2:8 ;
hence x,y to_power (j + 1) = x,y to_power (m + 1) by A2, A3, Def3; :: thesis: verum