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