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