let n be natural even number ; (- 1) |^ n = 1
defpred S1[ Nat] means ( $1 is even implies (- 1) |^ $1 = 1 );
A1:
now for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[b1] )assume A2:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[b1] end;
for k being Nat holds S1[k]
from NAT_1:sch 4(A1);
hence
(- 1) |^ n = 1
; verum