A1: ( <*0*> ^ <*1,3,3,1*> = <*0,1,3,3,1*> & <*1,3,3,1*> ^ <*0*> = <*1,3,3,1,0*> ) by FINSEQ_4:75;
Newton_Coeff (3 + 1) = <*0,1,3,3,1*> + <*1,3,3,1,0*> by A1, PT, NC3
.= <*(0 + 1),(1 + 3),(3 + 3),(3 + 1),(1 + 0)*> by A5B5 ;
hence Newton_Coeff 4 = <*1,4,6,4,1*> ; :: thesis: verum