theorem Th17: :: BCIALG_5:17

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n
for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k