for a, b being Real
for s being natural Number holds (a + b) |^ s = Sum ((a,b) In_Power s)