theorem INS: :: NEWTON04:57

for a, b being Real
for n being Nat holds (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n)