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