theorem Th38: :: NEWTON02:136

for m, n being Nat st m in dom (((Newton_Coeff n) | n) /^ 1) holds
(((Newton_Coeff n) | n) /^ 1) . m = (Newton_Coeff n) . (m + 1)