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:129;
(a * b) #R c = (a #R c) * (b #R c) by A1, A2, PREPOWER:78;
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