let a, b be Real; :: thesis: for n being odd Nat holds
( a |^ n = b |^ n iff a = b )
let n be odd Nat; :: thesis: ( a |^ n = b |^ n iff a = b )

per cases ( a >= 0 or a < 0 ) ;

suppose A1: a >= 0 ; :: thesis: ( a |^ n = b |^ n iff a = b )

per cases ( b >= 0 or b < 0 ) ;

suppose b >= 0 ; :: thesis: ( a |^ n = b |^ n iff a = b )

hence ( a |^ n = b |^ n iff a = b ) by A1, POW1; :: thesis: verum

end;

suppose b < 0 ; :: thesis: ( a |^ n = b |^ n iff a = b )

hence ( a |^ n = b |^ n iff a = b ) by A1; :: thesis: verum

end;

end;

end;

suppose A2: a < 0 ; :: thesis: ( a |^ n = b |^ n iff a = b )

per cases ( b < 0 or b >= 0 ) ;

suppose b < 0 ; :: thesis: ( a |^ n = b |^ n iff a = b )

then reconsider k = - b as positive Real ;
reconsider l = - a as positive Real by A2;
B1: ( (- a) |^ n = - (a |^ n) & (- b) |^ n = - (b |^ n) ) by POWER:2;
( k |^ n = l |^ n iff k = l ) by POW1;
hence ( a |^ n = b |^ n iff a = b ) by B1; :: thesis: verum

end;

suppose b >= 0 ; :: thesis: ( a |^ n = b |^ n iff a = b )

hence ( a |^ n = b |^ n iff a = b ) by A2; :: thesis: verum

end;

end;

end;

end;