Newton_Coeff (7 + 1) = (<*0*> ^ <*1,7,21,35,35,21,7,1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by PT, NC7
.= (<*0*> ^ (<*1,7,21,35,35*> ^ <*21,7,1*>)) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by AOFA_A00:def 6
.= ((<*0*> ^ <*1,7,21,35,35*>) ^ <*21,7,1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_1:32
.= ((<*0*> ^ (<*1,7,21,35*> ^ <*35*>)) ^ <*21,7,1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_4:75
.= (((<*0*> ^ <*1,7,21,35*>) ^ <*35*>) ^ <*21,7,1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_1:32
.= ((<*0,1,7,21,35*> ^ <*35*>) ^ <*21,7,1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_4:75
.= (<*0,1,7,21,35*> ^ (<*35*> ^ <*21,7,1*>)) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_1:32
.= (<*0,1,7,21,35*> ^ <*35,21,7,1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_4:74
.= (<*0,1,7,21,35*> ^ (<*35,21,7*> ^ <*1*>)) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_4:74
.= ((<*0,1,7,21,35*> ^ <*35,21,7*>) ^ <*1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by FINSEQ_1:32
.= (<*0,1,7,21,35,35,21,7*> ^ <*1*>) + (<*1,7,21,35,35,21,7,1*> ^ <*0*>) by AOFA_A00:def 6
.= (<*0,1,7,21,35,35,21,7*> + <*1,7,21,35,35,21,7,1*>) ^ <*(0 + 1)*> by FINSEQ_9:40
.= <*(0 + 1),(1 + 7),(7 + 21),(21 + 35),(35 + 35),(35 + 21),(21 + 7),(7 + 1)*> ^ <*(0 + 1)*> by A8B8 ;
hence Newton_Coeff 8 = <*1,8,28,56,70,56,28,8,1*> ; :: thesis: verum