theorem Th4: :: BCIALG_2:4

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