let X be BCI-algebra; :: thesis: for x being Element of X
for n being Nat st x in BCK-part X & n >= 1 holds
x |^ n = x
let x be Element of X; :: thesis: for n being Nat st x in BCK-part X & n >= 1 holds
x |^ n = x
let n be Nat; :: thesis: ( x in BCK-part X & n >= 1 implies x |^ n = x )
assume that
A1: x in BCK-part X and
A2: n >= 1 ; :: thesis: x |^ n = x
defpred S₁[ Nat] means x |^ $1 = x;
A3: ex y being Element of X st
( y = x & 0. X <= y ) by A1;

A4: now :: thesis: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume n >= 1 ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then x |^ (n + 1) = x \ (x `) by Th2
.= x \ (0. X) by A3
.= x by BCIALG_1:2 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A5: S₁[1] by Th4;
for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A5, A4);
hence x |^ n = x by A2; :: thesis: verum