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
per cases ( a > 0 or a = 0 ) by A1;
suppose A5: a > 0 ; :: thesis: contradiction
then A6: m -Root a > 0 by ;
then A7: n -Root (m -Root a) > 0 by ;
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 ;
then A10: (n * m) -Root a > 0 by ;
per cases ( n -Root (m -Root a) < (n * m) -Root a or (n * m) -Root a < n -Root (m -Root a) ) by ;
suppose n -Root (m -Root a) < (n * m) -Root a ; :: thesis: contradiction
end;
suppose (n * m) -Root a < n -Root (m -Root a) ; :: thesis: contradiction
end;
end;
end;
suppose A11: a = 0 ; :: thesis: contradiction
end;
end;