reconsider f = <*1,3,3*> as 3 -element real-valued FinSequence ;
len (Newton_Coeff 3) = 3 + 1 by NEWTON:def 5;
then ( dom (Newton_Coeff 3) = Seg 4 & (Newton_Coeff 3) . 1 = 1 & (Newton_Coeff 3) . (3 + 1) = 1 & (Newton_Coeff 3) . 2 = 3 & (Newton_Coeff 3) . 3 = 3 ) by FINSEQ_1:def 3;
hence Newton_Coeff 3 = <*1,3,3,1*> ; :: thesis: verum