1 in Seg 1 ;
then ( len (idseq 1) = 1 & (idseq 1) . 1 = 1 ) by CARD_1:def 7, FUNCT_1:18;
hence idseq 1 = <*1*> by FINSEQ_1:40; :: thesis: verum