theorem :: POWER:25

for a being Real holds a to_power 1 = a