let a, b, c be real number ; :: thesis: ( a > 0 implies (a to_power b) to_power c = a to_power (b * c) )
assume A1: a > 0 ; :: thesis: (a to_power b) to_power c = a to_power (b * c)
A2: a #R b > 0 by A1, PREPOWER:95;
A3: (a #R b) #R c = a #R (b * c) by A1, PREPOWER:105;
A4: (a #R b) #R c = a to_power (b * c) by A1, A3, Def2;
A5: (a #R b) to_power c = a to_power (b * c) by A2, A4, Def2;
thus (a to_power b) to_power c = a to_power (b * c) by A1, A5, Def2; :: thesis: verum