reconsider h = <*2,3*> as FinSequence of NAT ;

( <*1*> ^ h = <*1,2,3*> & Rev h = <*3,2*> ) by FINSEQ_1:43, FINSEQ_5:61;

hence Rev (idseq 3) = <*3,2,1*> by FINSEQ_2:53, FINSEQ_6:24; :: thesis: verum

( <*1*> ^ h = <*1,2,3*> & Rev h = <*3,2*> ) by FINSEQ_1:43, FINSEQ_5:61;

hence Rev (idseq 3) = <*3,2,1*> by FINSEQ_2:53, FINSEQ_6:24; :: thesis: verum