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

A2: now

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

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

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, A5, PREPOWER:28; :: thesis: verum

end;

now

assume B1: not n is even ; :: thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
then A11: ex m being Element of NAT st n = (2 * m) + 1 by ABIAN:9;
A12: n >= 1 by B1, ABIAN:12;

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

end;

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

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