for a, b, m, n being Nat holds Sum ((a,b) In_Power (m + n)) = (Sum ((a,b) In_Power m)) * (Sum ((a,b) In_Power n))