for a being Real holds a to_power 1 = a