for a being Real holds 1 to_power a = 1