let a, c be real positive number ; :: thesis: for b being real number holds (a / c) to_power (- b) = (c / a) to_power b
let b be real number ; :: 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