reconsider f = Hartr 6 as 6 -element complex-valued FinSequence ;
reconsider g = RHartr 6 as 6 -element complex-valued FinSequence ;
A1: ( g . 1 = 6 & g . 2 = 30 & g . 3 = 60 & g . 4 = 60 & g . 5 = 30 & g . 6 = 6 ) by RH6;
( len f = 6 & len g = 6 ) by CARD_1:def 7;
then ( dom f = Seg 6 & dom g = Seg 6 ) 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 ) ;
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) " ) by VALUED_1:def 7;
hence Hartr 6 = <*(1 / 6),(1 / 30),(1 / 60),(1 / 60),(1 / 30),(1 / 6)*> by A1; :: thesis: verum