A1: <*1,5,10,10,5,1*> = <*1,5,10,10,5*> ^ <*1*> by AOFA_A00:def 4;
then A2: <*0*> ^ <*1,5,10,10,5,1*> = (<*0*> ^ <*1,5,10,10,5*>) ^ <*1*> by FINSEQ_1:32
.= (<*0*> ^ (<*1,5,10,10*> ^ <*5*>)) ^ <*1*> by FINSEQ_4:75
.= ((<*0*> ^ <*1,5,10,10*>) ^ <*5*>) ^ <*1*> by FINSEQ_1:32
.= (<*0*> ^ <*1,5,10,10*>) ^ (<*5*> ^ <*1*>) by FINSEQ_1:32
.= <*0,1,5,10,10*> ^ <*5,1*> by FINSEQ_4:75 ;
A3: <*1,5,10,10,5,1*> ^ <*0*> = <*1,5,10,10,5*> ^ <*1,0*> by A1, FINSEQ_1:32;
A4: ( <*0*> ^ <*1,5,10,10,5,1*> = <*0,1,5,10,10,5,1*> & <*1,5,10,10,5,1*> ^ <*0*> = <*1,5,10,10,5,1,0*> ) by A2, A3, AOFA_A00:def 5;
Newton_Coeff (5 + 1) = <*0,1,5,10,10,5,1*> + <*1,5,10,10,5,1,0*> by A4, PT, NC5
.= <*(0 + 1),(1 + 5),(5 + 10),(10 + 10),(10 + 5),(5 + 1),(1 + 0)*> by A7B7 ;
hence Newton_Coeff 6 = <*1,6,15,20,15,6,1*> ; :: thesis: verum