let s be natural Number ; :: thesis: 2 |^ s = Sum (Newton_Coeff s)
2 |^ s = (1 + 1) |^ s
.= Sum ((1,1) In_Power s) by Th30
.= Sum (Newton_Coeff s) by Th31 ;
hence 2 |^ s = Sum (Newton_Coeff s) ; :: thesis: verum