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:37
.= ((c / a) * 1) to_power b by XCMPLX_1:81
.= (c / a) to_power b ;
hence (a / c) to_power (- b) = (c / a) to_power b ; :: thesis: verum