let a, b be Real; :: thesis: for n being Nat st a >= 0 & b >= 0 & n >= 1 holds
n -Root (a * b) = (n -Root a) * (n -Root b)

let n be Nat; :: thesis: ( a >= 0 & b >= 0 & n >= 1 implies n -Root (a * b) = (n -Root a) * (n -Root b) )
assume that
A1: a >= 0 and
A2: b >= 0 and
A3: n >= 1 and
A4: n -Root (a * b) <> (n -Root a) * (n -Root b) ; :: thesis: contradiction
A5: ((n -Root a) * (n -Root b)) |^ n = ((n -Root a) |^ n) * ((n -Root b) |^ n) by NEWTON:7
.= a * ((n -Root b) |^ n) by A1, A3, Th19
.= a * b by A2, A3, Th19 ;
per cases ( ( a > 0 & b > 0 ) or ( a = 0 & b > 0 ) or ( a > 0 & b = 0 ) or ( a = 0 & b = 0 ) ) by A1, A2;
suppose A6: ( a > 0 & b > 0 ) ; :: thesis: contradiction
then A7: n -Root b > 0 by ;
A8: n -Root a > 0 by A3, A6, Def2;
a * b > 0 by A6;
then A9: n -Root (a * b) > 0 by ;
per cases ( n -Root (a * b) < (n -Root a) * (n -Root b) or n -Root (a * b) > (n -Root a) * (n -Root b) ) by ;
suppose n -Root (a * b) < (n -Root a) * (n -Root b) ; :: thesis: contradiction
end;
suppose n -Root (a * b) > (n -Root a) * (n -Root b) ; :: thesis: contradiction
end;
end;
end;
suppose A10: ( a = 0 & b > 0 ) ; :: thesis: contradiction
end;
suppose A11: ( a > 0 & b = 0 ) ; :: thesis: contradiction
end;
suppose A12: ( a = 0 & b = 0 ) ; :: thesis: contradiction
end;
end;