let a be Real; :: thesis: for m, n being Nat st a >= 0 & n >= 1 & m >= 1 holds

n -Root (m -Root a) = (n * m) -Root a

let m, n be Nat; :: thesis: ( a >= 0 & n >= 1 & m >= 1 implies n -Root (m -Root a) = (n * m) -Root a )

assume that

A1: a >= 0 and

A2: n >= 1 and

A3: m >= 1 and

A4: n -Root (m -Root a) <> (n * m) -Root a ; :: thesis: contradiction

n -Root (m -Root a) = (n * m) -Root a

let m, n be Nat; :: thesis: ( a >= 0 & n >= 1 & m >= 1 implies n -Root (m -Root a) = (n * m) -Root a )

assume that

A1: a >= 0 and

A2: n >= 1 and

A3: m >= 1 and

A4: n -Root (m -Root a) <> (n * m) -Root a ; :: thesis: contradiction

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

end;

suppose A5:
a > 0
; :: thesis: contradiction

then A6:
m -Root a > 0
by A3, Def2;

then A7: n -Root (m -Root a) > 0 by A2, Def2;

A8: (n -Root (m -Root a)) |^ (n * m) = ((n -Root (m -Root a)) |^ n) |^ m by NEWTON:9

.= (m -Root a) |^ m by A2, A6, Lm2

.= a by A1, A3, Th19 ;

A9: n * m >= 1 by A2, A3, XREAL_1:159;

then A10: (n * m) -Root a > 0 by A5, Def2;

end;then A7: n -Root (m -Root a) > 0 by A2, Def2;

A8: (n -Root (m -Root a)) |^ (n * m) = ((n -Root (m -Root a)) |^ n) |^ m by NEWTON:9

.= (m -Root a) |^ m by A2, A6, Lm2

.= a by A1, A3, Th19 ;

A9: n * m >= 1 by A2, A3, XREAL_1:159;

then A10: (n * m) -Root a > 0 by A5, Def2;