let a, b be Complex; :: thesis: for n being natural Number holds (b / a) |^ n = (b |^ n) / (a |^ n)
let n be natural Number ; :: thesis: (b / a) |^ n = (b |^ n) / (a |^ n)
thus (b / a) |^ n = (b * (a ")) |^ n
.= (b |^ n) * ((a ") |^ n) by NEWTON:7
.= (b |^ n) * ((1 / a) |^ n)
.= (b |^ n) * (1 / (a |^ n)) by Th7
.= ((b |^ n) * 1) / (a |^ n)
.= (b |^ n) / (a |^ n) ; :: thesis: verum