let R be Ring; :: thesis: for a being Element of R
for n being odd Nat holds (- a) |^ n = - (a |^ n)
let a be Element of R; :: thesis: for n being odd Nat holds (- a) |^ n = - (a |^ n)
let n be odd Nat; :: thesis: (- a) |^ n = - (a |^ n)
defpred S₁[ Nat] means ( $1 is odd implies (- a) |^ $1 = - (a |^ $1) );

A: 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 A4: k = 1 ; :: thesis: S₁[k]

then (- a) |^ k = - a by BINOM:8
.= - (a |^ k) by A4, BINOM:8 ;
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;
(- a) |^ k = (- a) |^ (k2 + 2)
.= ((- a) |^ k2) * ((- a) |^ 2) by BINOM:10
.= (- (a |^ k2)) * ((- a) |^ (1 + 1)) by A2, A5, A4, NAT_1:16
.= (- (a |^ k2)) * (((- a) |^ 1) * ((- a) |^ 1)) by BINOM:10
.= (- (a |^ k2)) * ((- a) * ((- a) |^ 1)) by BINOM:8
.= (- (a |^ k2)) * ((- a) * (- a)) by BINOM:8
.= (- (a |^ k2)) * (a * a) by VECTSP_1:10
.= (- (a |^ k2)) * (- (- (a |^ 2))) by RING_5:3
.= (a |^ k2) * (- (a |^ 2)) by VECTSP_1:10
.= - ((a |^ k2) * (a |^ 2)) by VECTSP_1:8
.= - (a |^ k) by A4, BINOM:10 ;
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(A);
hence (- a) |^ n = - (a |^ n) ; :: thesis: verum