reconsider f = RHartr 6 as 6 -element FinSequence ;
reconsider g = Newton_Coeff (6 - 1) as 5 + 1 -element complex-valued FinSequence ;
A1: ( f . 1 = 6 * (g . 1) & f . 2 = 6 * (g . 2) & f . 3 = 6 * (g . 3) & f . 4 = 6 * (g . 4) & f . 5 = 6 * (g . 5) & f . 6 = 6 * (g . 6) ) by VALUED_1:6;
( g . 1 = 1 & g . 2 = 5 & g . 3 = 10 & g . 4 = 10 & g . 5 = 5 & g . 6 = 1 ) by NC5;
hence RHartr 6 = <*6,30,60,60,30,6*> by A1; :: thesis: verum