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 ;

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;

end;

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;

end;A8: n -Root a > 0 by A3, A6, Def2;

a * b > 0 by A6;

then A9: n -Root (a * b) > 0 by A3, Def2;