let a, b be Real; :: thesis: for c being Nat holds (a / b) to_power c = (a to_power c) / (b to_power c)
let c be Nat; :: thesis: (a / b) to_power c = (a to_power c) / (b to_power c)
(a / b) to_power c = (a * (1 / b)) |^ c by XCMPLX_1:99
.= (a to_power c) * ((1 / b) |^ c) by NEWTON:7
.= (a to_power c) * (1 / (b |^ c)) by PREPOWER:7
.= (a to_power c) / (b |^ c) by XCMPLX_1:99 ;
hence (a / b) to_power c = (a to_power c) / (b to_power c) ; :: thesis: verum