for X being BCI-algebra
for x, y, u being Element of X
for k being Nat
for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds
[x,((y,u) to_power k)] in E