let a, b be real number ; :: thesis: for n being Element of NAT st ( ( n >= 1 & a >= 0 & b >= 0 ) or ex m being Element of NAT st n = (2 * m) + 1 ) holds
n -root (a * b) = (n -root a) * (n -root b)
let n be Element of NAT ; :: thesis: ( ( ( n >= 1 & a >= 0 & b >= 0 ) or ex m being Element of NAT st n = (2 * m) + 1 ) implies n -root (a * b) = (n -root a) * (n -root b) )
assume A1: ( ( n >= 1 & a >= 0 & b >= 0 ) or ex m being Element of NAT st n = (2 * m) + 1 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

A2: now

let a, b be real number ; :: thesis: for n being Element of NAT st n >= 1 & a >= 0 & b >= 0 holds
n -root (a * b) = (n -root a) * (n -root b)
let n be Element of NAT ; :: thesis: ( n >= 1 & a >= 0 & b >= 0 implies n -root (a * b) = (n -root a) * (n -root b) )
assume A3: ( n >= 1 & a >= 0 & b >= 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)
thus n -root (a * b) = n -Root (a * b) by A3, Def1
.= (n -Root a) * (n -Root b) by A3, PREPOWER:31
.= (n -root a) * (n -Root b) by A3, Def1
.= (n -root a) * (n -root b) by A3, Def1 ; :: thesis: verum

end;

now

assume A4: ex m being Element of NAT st n = (2 * m) + 1 ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)
then consider m being Element of NAT such that
A5: n = (2 * m) + 1 ;
A6: n >= 0 + 1 by A5, XREAL_1:8;

now

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

suppose ( a >= 0 & b >= 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

hence n -root (a * b) = (n -root a) * (n -root b) by A2, A6; :: thesis: verum

end;

suppose A7: ( a < 0 & b < 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

then A8: a * b >= 0 ;
A9: - a >= 0 by A7;
A10: - b >= 0 by A7;
thus n -root (a * b) = n -Root ((- a) * (- b)) by A6, A8, Def1
.= (- (- (n -Root (- a)))) * (n -Root (- b)) by A6, A9, A10, PREPOWER:31
.= (- (n -root a)) * (- (- (n -Root (- b)))) by A4, A7, Def1
.= (- (n -root a)) * (- (n -root b)) by A4, A7, Def1
.= (n -root a) * (n -root b) ; :: thesis: verum

end;

suppose A11: ( a >= 0 & b < 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

thus n -root (a * b) = - (n -root (- (a * b))) by A4, Th11
.= - (n -root (a * (- b)))
.= - ((n -root a) * (n -root (- b))) by A2, A6, A11
.= (n -root a) * (- (n -root (- b)))
.= (n -root a) * (n -root b) by A4, Th11 ; :: thesis: verum

end;

suppose A13: ( a < 0 & b >= 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

thus n -root (a * b) = - (n -root (- (a * b))) by A4, Th11
.= - (n -root ((- a) * b))
.= - ((n -root (- a)) * (n -root b)) by A2, A6, A13
.= (- (n -root (- a))) * (n -root b)
.= (n -root a) * (n -root b) by A4, Th11 ; :: thesis: verum

end;

end;

end;

hence n -root (a * b) = (n -root a) * (n -root b) ; :: thesis: verum

end;

hence n -root (a * b) = (n -root a) * (n -root b) by A1, A2; :: thesis: verum