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