thus idseq 2 = idseq (1 + 1)
.= <*1,2*> by Th59, Th60 ; :: thesis: verum