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 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:141;
A4: (a / b) #R c = (a #R c) / (b #R c) by A1, A2, PREPOWER:94;
A5: (a / b) #R c = (a #R c) / (b to_power c) by A2, A4, Def2;
A6: (a / b) #R c = (a to_power c) / (b to_power c) by A1, A5, Def2;
thus (a / b) to_power c = (a to_power c) / (b to_power c) by A3, A6, Def2; :: thesis: verum