Sum (idseq n) is natural ;
hence Sum (idseq n) is Nat ; :: thesis: verum