:: deftheorem defines Subnomial NEWTON04:def 1 :
for a, b being Real
for n being natural Number holds (a,b) Subnomial n = ((a,b) In_Power n) /" (Newton_Coeff n);