let n be Element of 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₁[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(0. X) |^ (m + 1) = 0. X;
A1: S₁[ 0 ] by Th22;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of NAT ; :: thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(0. X) |^ (m + 1) = 0. X ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(0. X) |^ (m + 1) = 0. X )
assume A3: for m being Element of NAT st m = k & m <= n holds
(0. X) |^ (m + 1) = 0. X ; :: thesis: for m being Element of NAT st m = k + 1 & m <= n holds
(0. X) |^ (m + 1) = 0. X
let m be Element of NAT ; :: thesis: ( m = k + 1 & m <= n implies (0. X) |^ (m + 1) = 0. X )
assume A4: ( m = k + 1 & m <= n ) ; :: thesis: (0. X) |^ (m + 1) = 0. X
then A5: (0. X) |^ (m + 1) = ((0. X) |^ (k + 1)) * (0. X) by Def6;
A6: (0. X) |^ 2 = 0. X by Th25;
k <= n by A4, NAT_1:13;
then (0. X) |^ (k + 1) = 0. X by A3;
hence (0. X) |^ (m + 1) = 0. X by A5, A6, Th23; :: thesis: verum

end;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (0. X) |^ (n + 1) = 0. X ; :: thesis: verum