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