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