let n be Element of NAT ; :: thesis: for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds x,a to_power n = x \ (a |^ n)
let X be BCI-Algebra_with_Condition(S); :: thesis: for x, a being Element of X holds x,a to_power n = x \ (a |^ n)
let x, a be Element of X; :: thesis: x,a to_power n = x \ (a |^ n)
defpred S₁[ set ] means for m being Element of NAT st m = $1 & m <= n holds
x,a to_power m = x \ (a |^ m);

now

let k be Element of NAT ; :: thesis: ( ( for m being Element of NAT st m = k & m <= n holds
x,a to_power m = x \ (a |^ m) ) implies for m being Element of NAT st m = k + 1 & m <= n holds
x,a to_power m = x \ (a |^ m) )
assume A1: for m being Element of NAT st m = k & m <= n holds
x,a to_power m = x \ (a |^ m) ; :: thesis: for m being Element of NAT st m = k + 1 & m <= n holds
x,a to_power m = x \ (a |^ m)
let m be Element of NAT ; :: thesis: ( m = k + 1 & m <= n implies x,a to_power m = x \ (a |^ m) )
assume that
A2: m = k + 1 and
A3: m <= n ; :: thesis: x,a to_power m = x \ (a |^ m)
A4: ( x,a to_power m = (x,a to_power k) \ a & k <= n ) by A2, A3, BCIALG_2:4, NAT_1:13;
x \ (a |^ m) = x \ ((a |^ k) * a) by A2, Def6
.= (x \ (a |^ k)) \ a by Th12 ;
hence x,a to_power m = x \ (a |^ m) by A1, A4; :: thesis: verum

end;

then A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
A6: S₁[ 0 ] by Lm7;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A5);
hence x,a to_power n = x \ (a |^ n) ; :: thesis: verum