let a, b be Real; :: thesis: for n being Nat st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) holds
n -root (a / b) = (n -root a) / (n -root b)
let n be Nat; :: thesis: ( ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) implies n -root (a / b) = (n -root a) / (n -root b) )
assume A1: ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) ; :: thesis: n -root (a / b) = (n -root a) / (n -root b)

now :: thesis: n -root (a / b) = (n -root a) / (n -root b)

per cases ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) by A1;

suppose A2: ( a >= 0 & b > 0 & n >= 1 ) ; :: thesis: n -root (a / b) = (n -root a) / (n -root b)

hence n -root (a / b) = n -Root (a / b) by Def1
.= (n -Root a) / (n -Root b) by A2, PREPOWER:24
.= (n -root a) / (n -Root b) by A2, Def1
.= (n -root a) / (n -root b) by A2, Def1 ;
:: thesis: verum

end;

suppose A3: ( b <> 0 & n is odd ) ; :: thesis: n -root (a / b) = (n -root a) / (n -root b)

thus n -root (a / b) = n -root (a * (1 / b))
.= (n -root a) * (n -root (1 / b)) by A3, Th11
.= (n -root a) * (1 / (n -root b)) by A3, Th12
.= (n -root a) / (n -root b) ; :: thesis: verum

end;

end;

end;

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