len (Newton_Coeff 2) = 2 + 1 by NEWTON:def 5;
then ( dom (Newton_Coeff 2) = Seg 3 & (Newton_Coeff 2) . 1 = 1 & (Newton_Coeff 2) . (2 + 1) = 1 & (Newton_Coeff 2) . 2 = 2 ) by FINSEQ_1:def 3;
hence Newton_Coeff 2 = <*1,2,1*> ; :: thesis: verum