reconsider f = RHartr 7 as 7 -element FinSequence ;
reconsider g = Newton_Coeff (7 - 1) as 6 + 1 -element complex-valued FinSequence ;
A1: ( f . 1 = 7 * (g . 1) & f . 2 = 7 * (g . 2) & f . 3 = 7 * (g . 3) & f . 4 = 7 * (g . 4) & f . 5 = 7 * (g . 5) & f . 6 = 7 * (g . 6) & f . 7 = 7 * (g . 7) ) by VALUED_1:6;
( g . 1 = 1 & g . 2 = 6 & g . 3 = 15 & g . 4 = 20 & g . 5 = 15 & g . 6 = 6 & g . 7 = 1 ) by NC6;
hence RHartr 7 = <*7,42,105,140,105,42,7*> by A1; :: thesis: verum