theorem :: FINSEQ_2:53

idseq 3 = <*1,2,3*> by Th49, Th50;