<*0*> ^ <*1,4,6,4,1*> = <*0*> ^ (<*1,4,6,4*> ^ <*1*>) by FINSEQ_4:75
.= (<*0*> ^ <*1,4,6,4*>) ^ <*1*> by FINSEQ_1:32
.= <*0,1,4,6,4*> ^ <*1*> by FINSEQ_4:75 ;
then A1: ( <*0*> ^ <*1,4,6,4,1*> = <*0,1,4,6,4,1*> & <*1,4,6,4,1*> ^ <*0*> = <*1,4,6,4,1,0*> ) by AOFA_A00:def 4;
Newton_Coeff (4 + 1) = <*0,1,4,6,4,1*> + <*1,4,6,4,1,0*> by A1, PT, NC4
.= <*(0 + 1),(1 + 4),(4 + 6),(6 + 4),(4 + 1),(1 + 0)*> by A6B6 ;
hence Newton_Coeff 5 = <*1,5,10,10,5,1*> ; :: thesis: verum