reconsider f = RHartr 4 as 4 -element FinSequence ;
( f . 1 = 4 * ((Newton_Coeff 3) . 1) & f . 2 = 4 * ((Newton_Coeff 3) . 2) & f . 3 = 4 * ((Newton_Coeff 3) . 3) & f . 4 = 4 * ((Newton_Coeff 3) . 4) ) by VALUED_1:6;
hence RHartr 4 = <*4,12,12,4*> ; :: thesis: verum