let X be BCI-algebra; :: thesis: 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

let x, y, u be Element of X; :: thesis: 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

let k be Nat; :: thesis: 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

let E be Congruence of X; :: thesis: ( [x,y] in E & u in Class (E,(0. X)) implies [x,((y,u) to_power k)] in E )
assume that
A1: [x,y] in E and
A2: u in Class (E,(0. X)) ; :: thesis: [x,((y,u) to_power k)] in E
defpred S1[ Nat] means [x,((y,u) to_power \$1)] in E;
ex z being object st
( [z,u] in E & z in {(0. X)} ) by ;
then A3: [(0. X),u] in E by TARSKI:def 1;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume [x,((y,u) to_power k)] in E ; :: thesis: S1[k + 1]
then [(x \ (0. X)),(((y,u) to_power k) \ u)] in E by ;
then [x,(((y,u) to_power k) \ u)] in E by BCIALG_1:2;
hence S1[k + 1] by Th4; :: thesis: verum
end;
A5: S1[ 0 ] by ;
for n being Nat holds S1[n] from NAT_1:sch 2(A5, A4);
hence [x,((y,u) to_power k)] in E ; :: thesis: verum