for a being Real holds a to_power 2 = a ^2