let a, b be real number ; :: thesis: for n being Element of NAT st a >= 0 & b >= 0 & n >= 1 holds
n -Root (a * b) = (n -Root a) * (n -Root b)
let n be Element of NAT ; :: thesis: ( a >= 0 & b >= 0 & n >= 1 implies n -Root (a * b) = (n -Root a) * (n -Root b) )
assume that
A1: ( a >= 0 & b >= 0 & n >= 1 ) and
A2: n -Root (a * b) <> (n -Root a) * (n -Root b) ; :: thesis: contradiction
A3: ((n -Root a) * (n -Root b)) |^ n = ((n -Root a) |^ n) * ((n -Root b) |^ n) by NEWTON:12
.= a * ((n -Root b) |^ n) by A1, Th28
.= a * b by A1, Th28 ;

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

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

then a * b > 0 by XREAL_1:131;
then A5: n -Root (a * b) > 0 by A1, Def3;
A6: n -Root a > 0 by A1, A4, Def3;
n -Root b > 0 by A1, A4, Def3;
then A7: (n -Root a) * (n -Root b) > (n -Root a) * 0 by A6, XREAL_1:70;

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

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

hence contradiction by A1, A3, A5, Th28; :: thesis: verum

end;

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

hence contradiction by A1, A3, A7, Th28; :: thesis: verum

end;

end;

end;

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

then n -Root (a * b) = 0 by A1, Def3;
hence contradiction by A2, A8; :: thesis: verum

end;

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

then n -Root (a * b) = 0 by A1, Def3;
hence contradiction by A2, A9; :: thesis: verum

end;

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

then n -Root (a * b) = 0 by A1, Def3;
hence contradiction by A2, A10; :: thesis: verum

end;

end;