let X be BCI-algebra; :: thesis: for x being Element of X
for n being Nat holds (x ` ) |^ n = (x |^ n) `
let x be Element of X; :: thesis: for n being Nat holds (x ` ) |^ n = (x |^ n) `
let n be Nat; :: thesis: (x ` ) |^ n = (x |^ n) `
defpred S₁[ Nat] means (x ` ) |^ $1 = (x |^ $1) ` ;
(x ` ) |^ 0 = 0. X by Def1
.= (0. X) ` by BCIALG_1:def 5 ;
then A1: S₁[ 0 ] by Def1;

A3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
(x ` ) |^ (n + 1) = (x ` ) \ (((x |^ n) ` ) ` ) by B1, Th1
.= (x \ ((x |^ n) ` )) ` by BCIALG_1:9
.= (x |^ (n + 1)) ` by Th1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence (x ` ) |^ n = (x |^ n) ` ; :: thesis: verum