let a be real number ; :: thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
n -Root (m -Root a) = (n * m) -Root a
let n, m be Element of NAT ; :: thesis: ( a >= 0 & n >= 1 & m >= 1 implies n -Root (m -Root a) = (n * m) -Root a )
assume that
A1: ( a >= 0 & n >= 1 & m >= 1 ) and
A2: n -Root (m -Root a) <> (n * m) -Root a ; :: thesis: contradiction

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

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

then A4: m -Root a > 0 by A1, Def3;
A5: (n -Root (m -Root a)) |^ (n * m) = ((n -Root (m -Root a)) |^ n) |^ m by NEWTON:14
.= (m -Root a) |^ m by A1, A4, Lm2
.= a by A1, Th28 ;
A6: n * m >= 1 by A1, XREAL_1:161;
A7: n -Root (m -Root a) > 0 by A1, A4, Def3;
A8: (n * m) -Root a > 0 by A3, A6, Def3;

per cases ( n -Root (m -Root a) < (n * m) -Root a or (n * m) -Root a < n -Root (m -Root a) ) by A2, XXREAL_0:1;

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

hence contradiction by A3, A5, A6, A7, Def3; :: thesis: verum

end;

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

hence contradiction by A3, A5, A6, A8, Def3; :: thesis: verum

end;

end;

end;

suppose A9: a = 0 ; :: thesis: contradiction

n * m >= 1 by A1, XREAL_1:161;
then A10: (n * m) -Root a = 0 by A9, Def3;
m -Root a = 0 by A1, A9, Def3;
hence contradiction by A1, A2, A10, Def3; :: thesis: verum

end;

end;