:: deftheorem defines RHartr NEWTON07:def 1 :
for n being non zero Nat holds RHartr n = n (#) (Newton_Coeff (n - 1));