theorem DIS: :: NEWTON04:79

for i, n being Nat
for a, b being Integer holds a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)