let n be 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_{1}[ set ] means for m being Nat st m = $1 & m <= n holds

(x,a) to_power m = x \ (a |^ m);

_{1}[k] holds

S_{1}[k + 1]
;

A6: S_{1}[ 0 ]
by Lm7;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A6, A5);

hence (x,a) to_power n = x \ (a |^ n) ; :: thesis: verum

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

(x,a) to_power m = x \ (a |^ m);

now :: thesis: for k being Nat st ( for m being Nat st m = k & m <= n holds

(x,a) to_power m = x \ (a |^ m) ) holds

for m being Nat st m = k + 1 & m <= n holds

(x,a) to_power m = x \ (a |^ m)

then A5:
for k being Nat st S(x,a) to_power m = x \ (a |^ m) ) holds

for m being Nat st m = k + 1 & m <= n holds

(x,a) to_power m = x \ (a |^ m)

let k be Nat; :: thesis: ( ( for m being Nat st m = k & m <= n holds

(x,a) to_power m = x \ (a |^ m) ) implies for m being Nat st m = k + 1 & m <= n holds

(x,a) to_power m = x \ (a |^ m) )

assume A1: for m being Nat st m = k & m <= n holds

(x,a) to_power m = x \ (a |^ m) ; :: thesis: for m being Nat st m = k + 1 & m <= n holds

(x,a) to_power m = x \ (a |^ m)

let m be 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 Th11 ;

hence (x,a) to_power m = x \ (a |^ m) by A1, A4; :: thesis: verum

end;(x,a) to_power m = x \ (a |^ m) ) implies for m being Nat st m = k + 1 & m <= n holds

(x,a) to_power m = x \ (a |^ m) )

assume A1: for m being Nat st m = k & m <= n holds

(x,a) to_power m = x \ (a |^ m) ; :: thesis: for m being Nat st m = k + 1 & m <= n holds

(x,a) to_power m = x \ (a |^ m)

let m be 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 Th11 ;

hence (x,a) to_power m = x \ (a |^ m) by A1, A4; :: thesis: verum

S

A6: S

for n being Nat holds S

hence (x,a) to_power n = x \ (a |^ n) ; :: thesis: verum