let a be Real; :: 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 that

A1: a >= 0 and

A2: n >= 1 ; :: thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )

( (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 that

A1: a >= 0 and

A2: n >= 1 ; :: thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )

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

end;

suppose A3:
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 A2, INT_1:5;

A4: 0 |^ n = 0 |^ (m + 1)

.= (0 |^ m) * (0 |^ 1) by NEWTON:8

.= (0 |^ m) * ((0 GeoSeq) . (0 + 1)) by Def1

.= (0 |^ m) * (((0 GeoSeq) . 0) * 0) by Th3

.= 0 ;

hence (n -Root a) |^ n = a by A2, A3, Def2; :: thesis: n -Root (a |^ n) = a

thus n -Root (a |^ n) = a by A2, A3, A4, Def2; :: thesis: verum

end;reconsider m = k - k1 as Element of NAT by A2, INT_1:5;

A4: 0 |^ n = 0 |^ (m + 1)

.= (0 |^ m) * (0 |^ 1) by NEWTON:8

.= (0 |^ m) * ((0 GeoSeq) . (0 + 1)) by Def1

.= (0 |^ m) * (((0 GeoSeq) . 0) * 0) by Th3

.= 0 ;

hence (n -Root a) |^ n = a by A2, A3, Def2; :: thesis: n -Root (a |^ n) = a

thus n -Root (a |^ n) = a by A2, A3, A4, Def2; :: thesis: verum