theorem Th5: :: BCIALG_2:5

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