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 A3, Def2;
A8: n -Root a > 0 by A3, A6, Def2;
a * b > 0 by A6;
then A9: n -Root (a * b) > 0 by A3, Def2;

per cases ( n -Root (a * b) < (n -Root a) * (n -Root b) or n -Root (a * b) > (n -Root a) * (n -Root b) ) by A4, XXREAL_0:1;

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

hence contradiction by A3, A5, A9, Th19; :: thesis: verum

end;

suppose n -Root (a * b) > (n -Root a) * (n -Root b) ; :: thesis: contradiction

hence contradiction by A3, A5, A8, A7, Th19; :: thesis: verum

end;

end;

end;

suppose A10: ( a = 0 & b > 0 ) ; :: thesis: contradiction

then n -Root (a * b) = 0 by A3, Def2;
hence contradiction by A4, A10; :: thesis: verum

end;

suppose A11: ( a > 0 & b = 0 ) ; :: thesis: contradiction

then n -Root (a * b) = 0 by A3, Def2;
hence contradiction by A4, A11; :: thesis: verum

end;

suppose A12: ( a = 0 & b = 0 ) ; :: thesis: contradiction

then n -Root (a * b) = 0 by A3, Def2;
hence contradiction by A4, A12; :: thesis: verum

end;

end;