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 )

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

assume A3: n -Root (a |^ n) <> a ; :: thesis: contradiction

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

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

assume A3: n -Root (a |^ n) <> a ; :: thesis: contradiction