reconsider f = Hartr 7 as 7 -element complex-valued FinSequence ;
reconsider g = RHartr 7 as 7 -element complex-valued FinSequence ;
A1: ( g . 1 = 7 & g . 2 = 42 & g . 3 = 105 & g . 4 = 140 & g . 5 = 105 & g . 6 = 42 & g . 7 = 7 ) by RH7;
( len f = 7 & len g = 7 ) by CARD_1:def 7;
then ( dom f = Seg 7 & dom g = Seg 7 ) by FINSEQ_1:def 3;
then ( 1 in dom f & 2 in dom f & 3 in dom f & 4 in dom f & 5 in dom f & 6 in dom f & 7 in dom f ) ;
then ( f . 1 = (g . 1) " & f . 2 = (g . 2) " & f . 3 = (g . 3) " & f . 4 = (g . 4) " & f . 5 = (g . 5) " & f . 6 = (g . 6) " & f . 7 = (g . 7) " ) by VALUED_1:def 7;
hence Hartr 7 = <*(1 / 7),(1 / 42),(1 / 105),(1 / 140),(1 / 105),(1 / 42),(1 / 7)*> by A1; :: thesis: verum