let a be real number ; :: thesis: for n being Nat st ( ( n >= 1 & a >= 0 ) or ex m being Element of NAT st n = (2 * m) + 1 ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )
let n be Nat; :: thesis: ( ( ( n >= 1 & a >= 0 ) or ex m being Element of NAT st n = (2 * m) + 1 ) implies ( (n -root a) |^ n = a & n -root (a |^ n) = a ) )
assume A1: ( ( n >= 1 & a >= 0 ) or ex m being Element of NAT st n = (2 * m) + 1 ) ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )

A2: now

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

now

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

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

hence a |^ n >= 0 by PREPOWER:13; :: 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, PREPOWER:28; :: thesis: verum

end;

now

assume A5: ex m being Element of NAT st n = (2 * m) + 1 ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
then consider m being Element of NAT such that
A6: n = (2 * m) + 1 ;
A7: n >= 0 + 1 by A6, XREAL_1:8;

now

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, A7; :: thesis: verum

end;

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

then A9: - a > 0 by XREAL_1:60;
thus (n -root a) |^ n = (- (n -Root (- a))) |^ n by A5, A8, Def1
.= - ((n -Root (- a)) |^ n) by A5, Th2
.= - (- a) by A7, A9, PREPOWER:28
.= a ; :: thesis: n -root (a |^ n) = a
(- a) |^ n > 0 by A9, PREPOWER:13;
then - (a |^ n) > 0 by A5, Th2;
then a |^ n < 0 ;
hence n -root (a |^ n) = - (n -Root (- (a |^ n))) by A5, Def1
.= - (n -Root ((- a) |^ n)) by A5, Th2
.= - (- a) by A7, A9, PREPOWER:28
.= 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