let n be Nat; :: thesis: for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X

let X be BCI-Algebra_with_Condition(S); :: thesis: (0. X) |^ (n + 1) = 0. X

defpred S_{1}[ set ] means for m being Nat st m = $1 & m <= n holds

(0. X) |^ (m + 1) = 0. X;

_{1}[k] holds

S_{1}[k + 1]
;

A7: S_{1}[ 0 ]
by Th21;

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

hence (0. X) |^ (n + 1) = 0. X ; :: thesis: verum

let X be BCI-Algebra_with_Condition(S); :: thesis: (0. X) |^ (n + 1) = 0. X

defpred S

(0. X) |^ (m + 1) = 0. X;

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

(0. X) |^ (m + 1) = 0. X ) holds

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

(0. X) |^ (m + 1) = 0. X

then A6:
for k being Nat st S(0. X) |^ (m + 1) = 0. X ) holds

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

(0. X) |^ (m + 1) = 0. X

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

(0. X) |^ (m + 1) = 0. X ) implies for m being Nat st m = k + 1 & m <= n holds

(0. X) |^ (m + 1) = 0. X )

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

(0. X) |^ (m + 1) = 0. X ; :: thesis: for m being Nat st m = k + 1 & m <= n holds

(0. X) |^ (m + 1) = 0. X

let m be Nat; :: thesis: ( m = k + 1 & m <= n implies (0. X) |^ (m + 1) = 0. X )

assume that

A2: m = k + 1 and

A3: m <= n ; :: thesis: (0. X) |^ (m + 1) = 0. X

k <= n by A2, A3, NAT_1:13;

then A4: (0. X) |^ (k + 1) = 0. X by A1;

A5: (0. X) |^ 2 = 0. X by Th24;

(0. X) |^ (m + 1) = ((0. X) |^ (k + 1)) * (0. X) by A2, Def6;

hence (0. X) |^ (m + 1) = 0. X by A5, A4, Th22; :: thesis: verum

end;(0. X) |^ (m + 1) = 0. X ) implies for m being Nat st m = k + 1 & m <= n holds

(0. X) |^ (m + 1) = 0. X )

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

(0. X) |^ (m + 1) = 0. X ; :: thesis: for m being Nat st m = k + 1 & m <= n holds

(0. X) |^ (m + 1) = 0. X

let m be Nat; :: thesis: ( m = k + 1 & m <= n implies (0. X) |^ (m + 1) = 0. X )

assume that

A2: m = k + 1 and

A3: m <= n ; :: thesis: (0. X) |^ (m + 1) = 0. X

k <= n by A2, A3, NAT_1:13;

then A4: (0. X) |^ (k + 1) = 0. X by A1;

A5: (0. X) |^ 2 = 0. X by Th24;

(0. X) |^ (m + 1) = ((0. X) |^ (k + 1)) * (0. X) by A2, Def6;

hence (0. X) |^ (m + 1) = 0. X by A5, A4, Th22; :: thesis: verum

S

A7: S

for n being Nat holds S

hence (0. X) |^ (n + 1) = 0. X ; :: thesis: verum