let i, j, m, n be Nat; :: thesis: for X being BCK-algebra of i,j,m,n

for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1)

let X be BCK-algebra of i,j,m,n; :: thesis: for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1)

let x, y be Element of X; :: thesis: (x,y) to_power (i + 1) = (x,y) to_power (n + 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 ((m + 1),n,(x \ y),x) = ((x \ y),(x \ (x \ y))) to_power n by BCIALG_2:5

.= ((x \ (x \ (x \ y))),(x \ (x \ y))) to_power n by BCIALG_1:8

.= (((x,(x \ (x \ y))) to_power 1),(x \ (x \ y))) to_power n by BCIALG_2:2

.= (x,(x \ (x \ y))) to_power (n + 1) by BCIALG_2:10

.= (x,y) to_power (n + 1) by BCIALG_2:8 ;

X is BCI-algebra of m,n,i,j by Th13;

then A3: X is BCI-algebra of m + 1,n,i,j + 1 by Th14;

Polynom (i,(j + 1),x,(x \ y)) = (x,(x \ (x \ y))) to_power (i + 1) by A1, BCIALG_2:5

.= (x,y) to_power (i + 1) by BCIALG_2:8 ;

hence (x,y) to_power (i + 1) = (x,y) to_power (n + 1) by A2, A3, Def3; :: thesis: verum

for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1)

let X be BCK-algebra of i,j,m,n; :: thesis: for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1)

let x, y be Element of X; :: thesis: (x,y) to_power (i + 1) = (x,y) to_power (n + 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 ((m + 1),n,(x \ y),x) = ((x \ y),(x \ (x \ y))) to_power n by BCIALG_2:5

.= ((x \ (x \ (x \ y))),(x \ (x \ y))) to_power n by BCIALG_1:8

.= (((x,(x \ (x \ y))) to_power 1),(x \ (x \ y))) to_power n by BCIALG_2:2

.= (x,(x \ (x \ y))) to_power (n + 1) by BCIALG_2:10

.= (x,y) to_power (n + 1) by BCIALG_2:8 ;

X is BCI-algebra of m,n,i,j by Th13;

then A3: X is BCI-algebra of m + 1,n,i,j + 1 by Th14;

Polynom (i,(j + 1),x,(x \ y)) = (x,(x \ (x \ y))) to_power (i + 1) by A1, BCIALG_2:5

.= (x,y) to_power (i + 1) by BCIALG_2:8 ;

hence (x,y) to_power (i + 1) = (x,y) to_power (n + 1) by A2, A3, Def3; :: thesis: verum