reconsider f = RHartr 8 as 8 -element FinSequence ;
reconsider g = Newton_Coeff (8 - 1) as 7 + 1 -element complex-valued FinSequence ;
A1: ( f . 1 = 8 * (g . 1) & f . 2 = 8 * (g . 2) & f . 3 = 8 * (g . 3) & f . 4 = 8 * (g . 4) & f . 5 = 8 * (g . 5) & f . 6 = 8 * (g . 6) & f . 7 = 8 * (g . 7) & f . 8 = 8 * (g . 8) ) by VALUED_1:6;
( g . 1 = 1 & g . 2 = 7 & g . 3 = 21 & g . 4 = 35 & g . 5 = 35 & g . 6 = 21 & g . 7 = 7 & g . 8 = 1 ) by NC7;
hence RHartr 8 = <*8,56,168,280,280,168,56,8*> by A1; :: thesis: verum