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