let n be even Nat; :: thesis: (- 1) |^ n = 1
defpred S₁[ Nat] means ( $1 is even implies (- 1) |^ $1 = 1 );

A1: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[b₁] )
assume A2: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[b₁]

per cases ( k is odd or k is even ) ;

suppose k is odd ; :: thesis: S₁[b₁]

hence S₁[k] ; :: thesis: verum

end;

suppose A3: k is even ; :: thesis: S₁[b₁]

now :: thesis: ( ( k = 0 & S₁[k] ) or ( k > 0 & S₁[k] ) )

per cases ( k = 0 or k > 0 ) ;

case k = 0 ; :: thesis: S₁[k]

hence S₁[k] by NEWTON:4; :: thesis: verum

end;

case A4: k > 0 ; :: thesis: S₁[k]

( 0 is even & 0 + 1 = 1 ) ;
then k - 2 in NAT by A3, A4, NAT_1:23, INT_1:5;
then reconsider k2 = k - 2 as Nat ;
A5: k2 + 2 = k ;
then A6: k2 is even by A3;
(- 1) |^ k = (- 1) |^ (k2 + 2)
.= ((- 1) |^ k2) * ((- 1) |^ 2) by NEWTON:8
.= 1 * ((- 1) |^ (1 + 1)) by A2, A6, A5, NAT_1:16
.= ((- 1) |^ 1) * (- 1) by NEWTON:6
.= (- 1) * (- 1) ;
hence S₁[k] ; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
hence (- 1) |^ n = 1 ; :: thesis: verum