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 ;
per cases ( a > 0 or a = 0 ) by A1;
suppose A7: a > 0 ; :: thesis: contradiction
then A8: m -Root a > 0 by ;
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 ;
then A11: (n * m) -Root (a |^ (n + m)) > 0 by ;
per cases ) * (m -Root a) < (n * m) -Root (a |^ (n + m)) or (n -Root a) * (m -Root a) > (n * m) -Root (a |^ (n + m)) ) by ;
suppose (n -Root a) * (m -Root a) < (n * m) -Root (a |^ (n + m)) ; :: thesis: contradiction
end;
suppose (n -Root a) * (m -Root a) > (n * m) -Root (a |^ (n + m)) ; :: thesis: contradiction
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 ;
A13: a |^ (n + m) = a |^ ((m1 + m) + 1)
.= (a |^ (m1 + m)) * a by NEWTON:6
.= 0 by A12 ;
n -Root a = 0 by ;
hence contradiction by A4, A6, A13, Def2; :: thesis: verum
end;
end;