let n be odd Nat; :: thesis: (- 1) |^ n = - 1
defpred S₁[ Nat] means ( $1 is odd 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 even or k is odd ) ;

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

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

end;

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

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

per cases ( k = 0 or k = 1 or k >= 2 ) by NAT_1:23;

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

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

end;

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

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

end;

case k >= 2 ; :: thesis: S₁[k]

then k - 2 in NAT by INT_1:5;
then reconsider k2 = k - 2 as Nat ;
A4: k2 + 2 = k ;
then A5: k2 is odd by A3;
(- 1) |^ k = (- 1) |^ (k2 + 2)
.= ((- 1) |^ k2) * ((- 1) |^ 2) by NEWTON:8
.= (- 1) * ((- 1) |^ (1 + 1)) by A2, A5, A4, NAT_1:16
.= ((- 1) * ((- 1) |^ 1)) * (- 1) by NEWTON:6
.= ((- 1) * (- 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