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;

A6: 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;

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

end;

A10: 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, Lm1;

A13: 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 )

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

end;

end;

end;

thus ( (n -root a) |^ n = a & n -root (a |^ n) = a ) by A13; :: thesis: verum

end;

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