A1: <*1,6,15,20,15,6,1*> = <*1,6,15,20,15*> ^ <*6,1*> by AOFA_A00:def 5;
then A2: <*0*> ^ <*1,6,15,20,15,6,1*> = (<*0*> ^ <*1,6,15,20,15*>) ^ <*6,1*> by FINSEQ_1:32
.= (<*0*> ^ (<*1,6,15,20*> ^ <*15*>)) ^ <*6,1*> by FINSEQ_4:75
.= ((<*0*> ^ <*1,6,15,20*>) ^ <*15*>) ^ <*6,1*> by FINSEQ_1:32
.= (<*0*> ^ <*1,6,15,20*>) ^ (<*15*> ^ <*6,1*>) by FINSEQ_1:32
.= (<*0*> ^ <*1,6,15,20*>) ^ <*15,6,1*> by FINSEQ_1:43
.= <*0,1,6,15,20*> ^ <*15,6,1*> by FINSEQ_4:75 ;
A3: <*1,6,15,20,15,6,1*> ^ <*0*> = <*1,6,15,20,15*> ^ <*6,1,0*> by A1, FINSEQ_1:32;
A4: ( <*0*> ^ <*1,6,15,20,15,6,1*> = <*0,1,6,15,20,15,6,1*> & <*1,6,15,20,15,6,1*> ^ <*0*> = <*1,6,15,20,15,6,1,0*> ) by A2, A3, AOFA_A00:def 6;
Newton_Coeff (6 + 1) = <*0,1,6,15,20,15,6,1*> + <*1,6,15,20,15,6,1,0*> by A4, PT, NC6
.= <*(0 + 1),(1 + 6),(6 + 15),(15 + 20),(20 + 15),(15 + 6),(6 + 1),(1 + 0)*> by A8B8 ;
hence Newton_Coeff 7 = <*1,7,21,35,35,21,7,1*> ; :: thesis: verum