let n be positive Nat; :: thesis: Sum (Newton_Coeff n) = (Sum (((Newton_Coeff n) | n) /^ 1)) + 2
Sum (Newton_Coeff n) = ((Sum (((Newton_Coeff n) | n) /^ 1)) + ((Newton_Coeff n) . 1)) + ((Newton_Coeff n) . (n + 1)) by Th34
.= ((Sum (((Newton_Coeff n) | n) /^ 1)) + ((Newton_Coeff n) . 1)) + 1 by Th32
.= ((Sum (((Newton_Coeff n) | n) /^ 1)) + 1) + 1 by Th33 ;
hence Sum (Newton_Coeff n) = (Sum (((Newton_Coeff n) | n) /^ 1)) + 2 ; :: thesis: verum