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