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