let a be Real; :: thesis: for m, n being Nat st a >= 0 & n >= 1 & m >= 1 holds
(n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m))
let m, n be Nat; :: thesis: ( a >= 0 & n >= 1 & m >= 1 implies (n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m)) )
assume that
A1: a >= 0 and
A2: n >= 1 and
A3: m >= 1 and
A4: (n -Root a) * (m -Root a) <> (n * m) -Root (a |^ (n + m)) ; :: thesis: contradiction
A5: ((n -Root a) * (m -Root a)) |^ (n * m) = ((n -Root a) |^ (n * m)) * ((m -Root a) |^ (n * m)) by NEWTON:7
.= (((n -Root a) |^ n) |^ m) * ((m -Root a) |^ (n * m)) by NEWTON:9
.= (a |^ m) * ((m -Root a) |^ (m * n)) by A1, A2, Th19
.= (a |^ m) * (((m -Root a) |^ m) |^ n) by NEWTON:9
.= (a |^ m) * (a |^ n) by A1, A3, Th19
.= a |^ (n + m) by NEWTON:8 ;
A6: n * m >= 1 by A2, A3, XREAL_1:159;

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

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

then A8: m -Root a > 0 by A3, Def2;
n -Root a > 0 by A2, A7, Def2;
then A9: (n -Root a) * (m -Root a) > 0 by A8;
A10: a |^ (n + m) > 0 by A7, Th6;
then A11: (n * m) -Root (a |^ (n + m)) > 0 by A6, Def2;

per cases ( (n -Root a) * (m -Root a) < (n * m) -Root (a |^ (n + m)) or (n -Root a) * (m -Root a) > (n * m) -Root (a |^ (n + m)) ) by A4, XXREAL_0:1;

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

hence contradiction by A5, A6, A10, A9, Def2; :: thesis: verum

end;

suppose (n -Root a) * (m -Root a) > (n * m) -Root (a |^ (n + m)) ; :: thesis: contradiction

hence contradiction by A5, A6, A10, A11, Def2; :: thesis: verum

end;

end;

end;

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

reconsider k = n, k1 = 1 as Integer ;
reconsider m1 = k - k1 as Element of NAT by A2, INT_1:5;
A13: a |^ (n + m) = a |^ ((m1 + m) + 1)
.= (a |^ (m1 + m)) * a by NEWTON:6
.= 0 by A12 ;
n -Root a = 0 by A2, A12, Def2;
hence contradiction by A4, A6, A13, Def2; :: thesis: verum

end;

end;