let b, a be real number ; :: 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 Th14
.= ((b |^ n) * 1) / (a |^ n)
.= (b |^ n) / (a |^ n) ; :: thesis: verum