reconsider n = n as Nat by TARSKI:1;
Seg n is natural-membered ;
hence idseq n is natural-valued ; :: thesis: verum