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