ex n being Element of NAT st dom p = n by Th7;
hence dom p is natural ; :: thesis: verum