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 S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
x,a to_power m = x \ (a |^ m);
A1:
S1[ 0 ]
by Lm7;
A2:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
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 A3:
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 A4:
(
m = k + 1 &
m <= n )
;
:: thesis: x,a to_power m = x \ (a |^ m)then A5:
x,
a to_power m = (x,a to_power k) \ a
by BCIALG_2:4;
A6:
x \ (a |^ m) =
x \ ((a |^ k) * a)
by A4, Def6
.=
(x \ (a |^ k)) \ a
by Th12
;
k <= n
by A4, NAT_1:13;
hence
x,
a to_power m = x \ (a |^ m)
by A3, A5, A6;
:: thesis: verum end;
hence
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
;
:: thesis: verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A1, A2);
hence
x,a to_power n = x \ (a |^ n)
; :: thesis: verum