let X be BCI-algebra; :: thesis: for x, y, u being Element of X
for k being Element of 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 Element of 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 Element of 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₁[ Element of NAT ] means [x,(y,u to_power $1)] in E;
ex z being set 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume [x,(y,u to_power k)] in E ; :: thesis: S₁[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₁[k + 1] by Th4; :: thesis: verum

end;

A5: S₁[ 0 ] by A1, Th1;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A4);
hence [x,(y,u to_power k)] in E ; :: thesis: verum