let a be real number ; :: thesis: for b, c being integer number st a <> 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)
let b, c be integer number ; :: thesis: ( a <> 0 implies a to_power (b + c) = (a to_power b) * (a to_power c) )
assume AA: 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:50
.= (a #Z b) * (a #Z c) by POWER:50
.= a #Z (b + c) by AA, PREPOWER:54
.= a to_power (b + c) by POWER:50 ; :: thesis: verum