let a be Real; :: thesis: for b, c being Integer st a <> 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)
let b, c be Integer; :: 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)
thus (a to_power b) * (a to_power c) = (a #Z b) * (a to_power c) by POWER:43
.= (a #Z b) * (a #Z c) by POWER:43
.= a #Z (b + c) by A1, PREPOWER:44
.= a to_power (b + c) by POWER:43 ; :: thesis: verum