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