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 and
A2: b > 0 and
A3: n >= 1 ; :: thesis: n -Root (a / b) = (n -Root a) / (n -Root b)
thus n -Root (a / b) = n -Root (a * (b "))
.= (n -Root a) * (n -Root (b ")) by A1, A2, A3, Th31
.= (n -Root a) * (n -Root (1 / b))
.= (n -Root a) * (1 / (n -Root b)) by A2, A3, Th32
.= ((n -Root a) * 1) / (n -Root b)
.= (n -Root a) / (n -Root b) ; :: thesis: verum