theorem Th7: :: BCIALG_2:7

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