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 A1: ( [x,y] in E & u in Class E,(0. X) ) ; :: thesis: [x,(y,u to_power k)] in E
then consider z being set such that
A2: ( [z,u] in E & z in {(0. X)} ) by RELAT_1:def 13;
A3: [(0. X),u] in E by A2, TARSKI:def 1;
defpred S₁[ Element of NAT ] means [x,(y,u to_power $1)] in E;
A4: S₁[ 0 ] by A1, Th1;
A5: 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;

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