((0,0) Subnomial n) . k = (((0,0) In_Power n) . k) / ((Newton_Coeff n) . k) by VALUED_1:17;
hence ((0,0) Subnomial n) . k is zero ; :: thesis: verum