let a be Real; :: thesis: for n being Nat st ( ( n >= 1 & a >= 0 ) or n is odd ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )
let n be Nat; :: thesis: ( ( ( n >= 1 & a >= 0 ) or n is odd ) implies ( (n -root a) |^ n = a & n -root (a |^ n) = a ) )
assume A1: ( ( n >= 1 & a >= 0 ) or n is odd ) ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )

A2: now :: thesis: ( n >= 1 & a >= 0 implies ( (n -root a) |^ n = a & n -root (a |^ n) = a ) )

assume that
A3: n >= 1 and
A4: a >= 0 ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
A5: n -root a = n -Root a by A3, A4, Def1;

now :: thesis: a |^ n >= 0

per cases ( a > 0 or a = 0 ) by A4;

suppose a > 0 ; :: thesis: a |^ n >= 0

hence a |^ n >= 0 by PREPOWER:6; :: thesis: verum

end;

suppose a = 0 ; :: thesis: a |^ n >= 0

hence a |^ n >= 0 ; :: thesis: verum

end;

end;

end;

then n -root (a |^ n) = n -Root (a |^ n) by A3, Def1;
hence ( (n -root a) |^ n = a & n -root (a |^ n) = a ) by A3, A4, A5, PREPOWER:19; :: thesis: verum

end;

now :: thesis: ( n is odd implies ( (n -root a) |^ n = a & n -root (a |^ n) = a ) )

assume A6: n is odd ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
then A7: ex m being Nat st n = (2 * m) + 1 by ABIAN:9;
A8: n >= 1 by A6, ABIAN:12;

now :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )

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

suppose a >= 0 ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )

hence ( (n -root a) |^ n = a & n -root (a |^ n) = a ) by A2, A8; :: thesis: verum

end;

suppose A9: a < 0 ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )

then A10: - a > 0 by XREAL_1:58;
thus (n -root a) |^ n = (- (n -Root (- a))) |^ n by A7, A9, Def1
.= - ((n -Root (- a)) |^ n) by A7, Th2
.= - (- a) by A8, A9, PREPOWER:19
.= a ; :: thesis: n -root (a |^ n) = a
(- a) |^ n > 0 by A10, PREPOWER:6;
then - (a |^ n) > 0 by A7, Th2;
then a |^ n < 0 ;
hence n -root (a |^ n) = - (n -Root (- (a |^ n))) by A7, Def1
.= - (n -Root ((- a) |^ n)) by A7, Th2
.= - (- a) by A8, A9, PREPOWER:19
.= a ;
:: thesis: verum

end;

end;

end;

hence ( (n -root a) |^ n = a & n -root (a |^ n) = a ) ; :: thesis: verum

end;

hence ( (n -root a) |^ n = a & n -root (a |^ n) = a ) by A1, A2; :: thesis: verum