theorem PT: :: NEWTON07:51

for n being Nat holds Newton_Coeff (n + 1) = (<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)