thus <*n*> is Element of 1 -tuples_on NAT by FINSEQ_2:131; :: thesis: verum