let a, b be Nat; :: thesis: for m being positive Nat holds Sum ((a,b) In_Power m) = ((a |^ m) + (b |^ m)) + (Sum ((((a,b) In_Power m) | m) /^ 1))
let m be positive Nat; :: thesis: Sum ((a,b) In_Power m) = ((a |^ m) + (b |^ m)) + (Sum ((((a,b) In_Power m) | m) /^ 1))
len ((a,b) In_Power m) = m + 1 by NEWTON:def 4;
then Sum ((a,b) In_Power m) = ((Sum ((((a,b) In_Power m) | m) /^ 1)) + (((a,b) In_Power m) . 1)) + (((a,b) In_Power m) . (m + 1)) by Th17
.= ((Sum ((((a,b) In_Power m) | m) /^ 1)) + (a |^ m)) + (((a,b) In_Power m) . (m + 1)) by NEWTON:28
.= ((Sum ((((a,b) In_Power m) | m) /^ 1)) + (a |^ m)) + (b |^ m) by NEWTON:29 ;
hence Sum ((a,b) In_Power m) = ((a |^ m) + (b |^ m)) + (Sum ((((a,b) In_Power m) | m) /^ 1)) ; :: thesis: verum