for n being Nat
for a, b, c being Real holds Sum (((a + b),c) In_Power n) = Sum ((a,(b + c)) In_Power n)