reconsider h = <*2,3*> as FinSequence of NAT ;
( <*1*> ^ h = <*1,2,3*> & Rev h = <*3,2*> ) by FINSEQ_1:60, FINSEQ_5:64;
hence Rev (idseq 3) = <*3,2,1*> by FINSEQ_2:62, FINSEQ_6:28; :: thesis: verum