let a be real number ; :: thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
(n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m))
let n, m be Element of 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 & n >= 1 & m >= 1 ) and
A2: (n -Root a) * (m -Root a) <> (n * m) -Root (a |^ (n + m)) ; :: thesis: contradiction
A3: ((n -Root a) * (m -Root a)) |^ (n * m) = ((n -Root a) |^ (n * m)) * ((m -Root a) |^ (n * m)) by NEWTON:12
.= (((n -Root a) |^ n) |^ m) * ((m -Root a) |^ (n * m)) by NEWTON:14
.= (a |^ m) * ((m -Root a) |^ (m * n)) by A1, Th28
.= (a |^ m) * (((m -Root a) |^ m) |^ n) by NEWTON:14
.= (a |^ m) * (a |^ n) by A1, Th28
.= a |^ (n + m) by NEWTON:13 ;
A4: n * m >= 1 by A1, XREAL_1:161;

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

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

then A6: a |^ (n + m) > 0 by Th13;
A7: n -Root a > 0 by A1, A5, Def3;
m -Root a > 0 by A1, A5, Def3;
then A8: (n -Root a) * (m -Root a) > 0 by A7, XREAL_1:131;
A9: (n * m) -Root (a |^ (n + m)) > 0 by A4, A6, Def3;

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 A2, XXREAL_0:1;

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

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

end;

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

hence contradiction by A3, A4, A6, A9, Def3; :: thesis: verum

end;

end;

end;

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

reconsider k = n, k1 = 1 as Integer ;
reconsider m1 = k - k1 as Element of NAT by A1, INT_1:18;
A11: a |^ (n + m) = a |^ ((m1 + m) + 1)
.= (a |^ (m1 + m)) * a by NEWTON:11
.= 0 by A10 ;
n -Root a = 0 by A1, A10, Def3;
hence contradiction by A2, A4, A11, Def3; :: thesis: verum

end;

end;