theorem NIS: :: NEWTON04:46

for n being Nat
for a, b being Integer
for k being Nat st k in dom (Newton_Coeff n) holds
(Newton_Coeff n) . k divides ((a,b) In_Power n) . k