let a, b, m, n be Nat; :: thesis: Sum ((a,b) In_Power (m + n)) = (Sum ((a,b) In_Power m)) * (Sum ((a,b) In_Power n))
Sum ((a,b) In_Power (m + n)) = (a + b) |^ (m + n) by NEWTON:30
.= ((a + b) |^ m) * ((a + b) |^ n) by NEWTON:8
.= (Sum ((a,b) In_Power m)) * ((a + b) |^ n) by NEWTON:30
.= (Sum ((a,b) In_Power m)) * (Sum ((a,b) In_Power n)) by NEWTON:30 ;
hence Sum ((a,b) In_Power (m + n)) = (Sum ((a,b) In_Power m)) * (Sum ((a,b) In_Power n)) ; :: thesis: verum