let a, b, c be Real; :: thesis: ( a > 0 & b > 0 implies (a / b) to_power c = (a to_power c) / (b to_power c) )
assume that
A1: a > 0 and
A2: b > 0 ; :: thesis: (a / b) to_power c = (a to_power c) / (b to_power c)
A3: a / b > 0 by A1, A2, XREAL_1:139;
(a / b) #R c = (a #R c) / (b #R c) by A1, A2, PREPOWER:80;
then (a / b) #R c = (a #R c) / (b to_power c) by A2, Def2;
then (a / b) #R c = (a to_power c) / (b to_power c) by A1, Def2;
hence (a / b) to_power c = (a to_power c) / (b to_power c) by A3, Def2; :: thesis: verum