theorem :: BCIALG_5:15

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