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)
then a #R (b - c) = (a #R b) / (a #R c) by PREPOWER:91;
then a #R (b - c) = (a #R b) / (a to_power c) by A1, Def2;
then a #R (b - c) = (a to_power b) / (a to_power c) by A1, Def2;
hence a to_power (b - c) = (a to_power b) / (a to_power c) by A1, Def2; :: thesis: verum