let a, c be positive Real; :: thesis: for b being Real holds (a / c) to_power (- b) = (c / a) to_power b
let b be Real; :: thesis: (a / c) to_power (- b) = (c / a) to_power b
(a / c) to_power (- b) = (1 / (a / c)) to_power b by POWER:32
.= ((c / a) * 1) to_power b by XCMPLX_1:80
.= (c / a) to_power b ;
hence (a / c) to_power (- b) = (c / a) to_power b ; :: thesis: verum