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 A1: ( x in BCK-part X & n >= 1 ) ; :: thesis: x |^ n = x
then consider y being Element of X such that
A3: ( y = x & 0. X <= y ) ;
defpred S₁[ Nat] means x |^ $1 = x;
B1: S₁[1] by Th3;

B3: now

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

end;

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