theorem Th4: :: BCIALG_5:4

for n being Nat
for X being BCK-algebra
for x being Element of X holds ((0. X),x) to_power n = 0. X