let s be Nat; :: thesis: 2 |^ s = Sum (Newton_Coeff s)
2 |^ s = (1 + 1) |^ s
.= Sum ((1,1) In_Power s) by Th41
.= Sum (Newton_Coeff s) by Th43 ;
hence 2 |^ s = Sum (Newton_Coeff s) ; :: thesis: verum