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 S_{1}[ Nat] means [x,((y,u) to_power $1)] in E;

ex z being object st

( [z,u] in E & z in {(0. X)} ) by A2, RELAT_1:def 13;

then A3: [(0. X),u] in E by TARSKI:def 1;

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A1, Th1;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A5, A4);

hence [x,((y,u) to_power k)] in E ; :: thesis: verum

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 S

ex z being object st

( [z,u] in E & z in {(0. X)} ) by A2, RELAT_1:def 13;

then A3: [(0. X),u] in E by TARSKI:def 1;

A4: for k being Nat st S

S

proof

A5:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume [x,((y,u) to_power k)] in E ; :: thesis: S_{1}[k + 1]

then [(x \ (0. X)),(((y,u) to_power k) \ u)] in E by A3, Def9;

then [x,(((y,u) to_power k) \ u)] in E by BCIALG_1:2;

hence S_{1}[k + 1]
by Th4; :: thesis: verum

end;assume [x,((y,u) to_power k)] in E ; :: thesis: S

then [(x \ (0. X)),(((y,u) to_power k) \ u)] in E by A3, Def9;

then [x,(((y,u) to_power k) \ u)] in E by BCIALG_1:2;

hence S

for n being Nat holds S

hence [x,((y,u) to_power k)] in E ; :: thesis: verum