let n be Nat; 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); for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n)
let x, a be Element of X; (x,a) to_power n = x \ (a |^ n)
defpred S1[ set ] means for m being Nat st m = $1 & m <= n holds
(x,a) to_power m = x \ (a |^ m);
now 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)let k be
Nat;
( ( 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)
;
for m being Nat st m = k + 1 & m <= n holds
(x,a) to_power m = x \ (a |^ m)let m be
Nat;
( m = k + 1 & m <= n implies (x,a) to_power m = x \ (a |^ m) )assume that A2:
m = k + 1
and A3:
m <= n
;
(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;
verum end;
then A5:
for k being Nat st S1[k] holds
S1[k + 1]
;
A6:
S1[ 0 ]
by Lm7;
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A5);
hence
(x,a) to_power n = x \ (a |^ n)
; verum