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

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

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

end;

suppose A2: a = 0 ; :: thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )

reconsider k = n, k1 = 1 as Integer ;
reconsider m = k - k1 as Element of NAT by A1, INT_1:18;
A3: 0 |^ n = 0 |^ (m + 1)
.= (0 |^ m) * (0 |^ 1) by NEWTON:13
.= (0 |^ m) * ((0 GeoSeq ) . (0 + 1)) by Def1
.= (0 |^ m) * (((0 GeoSeq ) . 0 ) * 0 ) by Th4
.= 0 ;
hence (n -Root a) |^ n = a by A1, A2, Def3; :: thesis: n -Root (a |^ n) = a
thus n -Root (a |^ n) = a by A1, A2, A3, Def3; :: thesis: verum

end;

end;