theorem :: POWER:43

for a being Real
for k being Integer holds a to_power k = a #Z k by Def2;