for a, b being positive Real
for n being Real holds
( (a + b) to_power n = (a to_power n) + (b to_power n) iff n = 1 )