theorem Th20: :: BCIALG_5:20

for i, j, m, n being Nat
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)