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