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