let a, b, c be real number ; :: thesis: ( a > 0 & b > 0 implies (a / b) to_power c = (a to_power c) / (b to_power c) )
assume A1: ( a > 0 & b > 0 ) ; :: thesis: (a / b) to_power c = (a to_power c) / (b to_power c)
then A2: a / b > 0 by XREAL_1:141;
(a / b) #R c = (a #R c) / (b #R c) by A1, PREPOWER:94;
then (a / b) #R c = (a #R c) / (b to_power c) by A1, 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 A2, Def2; :: thesis: verum